144 3 Der Redehandlungskalkul
Theorem 3-19. VERS, VANS, VER und VAN bei SE
Wenn S ∈ SEQ und S' ∈ SEF(S), dann:
(i) {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)} ist ein SE-geschlossener Abschnitt in
S',
(ii) VERS(S)WErS(W) ⊂ {(j, S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)},
(iii) VERS(S') = (VERS(S)∖{(j, S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)}) и
{(Dom(S), S Dom(S))},
(iv) VANS(S)∖VANS(S') = {(max(Dom(VANS(S))), s'. .. , );_
(v) VANS(S) = VANS(S') и {(max(Dom(VANS(S))), S'max(Dom(VANS(S))))},
(vi) VER(S)∖VER(S') ⊂ {A(S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)},
(vii) VER(S) ⊂ {A(S'j) | j ∈ Dom(VERS(S')fDom(S))} и
{A(S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)},
(Viii) VAN(S)∖VAN(S') ⊂ {A(S'max(Dom(VANS(S))))},
(ix) VAN(S) = VAN(S') и {A(S'max(Dom(VANS(S))))} Und
(x) K(S') = rA(S'max(Dom(VΛNS(S)))) → K(SΓ ∙
Beweis: Sei S ∈ SEQ und S' ∈ SEF(S)∙ Dann gilt mit Definition 3-18 S' ∈ RGF(S)∙ So-
dann gilt mit Definition 3-2: Es gibt Δ, Γ ∈ GFORM und i ∈ Dom(S), so dass A(Si) = Δ
und (i, Si) ∈ VANS(S) und A(SDom(S)—1) = Γ und es kein l mit i < l ≤ Dom(S)-I gibt, so
dass (l, Sl) ∈ VANS(S) und S' = S и {(Dom(S), rAlso Δ → Γ)} und somit S' ∈ SEQ
und S'ΓDom(S')-1 = SlDom(S) = S∙
Sodann ist ® = {(j, S'j) | i ≤ j ≤ Dom(S)} ein Abschnitt in S' und A(S'i) = Δ und (i, S'i)
∈ VANS(S'ΓDom(S)) und A(S Dom(S)-i) Γ und es gibt kein l mit i < l ≤ ^Do^n(S)-1, so
dass (l, S'l) ∈ VANS(S'ΓDom(S)) und A(S'Dom(S)) = r∆ → Γ1∙ Damit gilt mit Theorem
2-91, dass ® ein SE-geschlossener und damit auch ein geschlossener Abschnitt in S' ist.
Da sodann max(Dom(Φ)) = Dom(S) = Dom(S')-1, ergibt sich mit Theorem 2-86,
dass VANS(SlDom(S')-1)WANS(S') = {(min(Dom(Φ)), S min(Dom(S))) }
{(max(Dom(VANS(SlDom(S')-1))), S'max(Dom(VANS(S'∣Dom(S')-1))))}∙ Da S = SlDom(S')-1
folgt daraus: VANS(S)∖VANS(S') = {(min(Dom(Φ)), S min(Dom(®)))}
{(max(Dom(VANS(S))), S'max(Dom(VANS(S))))}∙ Damit ist i = mi n( Dom(4B)) =
max(Dom(VANS(S))) und es gilt: ® = {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)}∙
Damit gilt dann (i). AuBerdem gilt dann A(S'max(Dom(vANS(S)))) = A(Si) = Δ und da K(S) =
Γ und K(S') = r∆ → Γπ gilt dann (x). Sodann ergibt sich mit VANS(S)∖VANS(S') ≠ 0
und Theorem 2-73 auch VERS(S)∖VERS(S') ≠ 0∙ Damit und mit S = S'ΓDom(S')-1 und
® = {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)} ergeben sich dann mit Theorem