3.3 VERS, VANS, VER und VAN in Ableitungen und bei einzelnen Ubergangen 145
2-83-(iv) bis -(xi) und mit der eindeutigen Bestimmtheit geschlossener Abschnitte mit
demselben Endglied (Theorem 2-53) die restlichen Klauseln ((ii) bis (ix)). ■
Theorem 3-20. VERS, VANS, VER und VAN bei NE
Wenn S ∈ SEQ und S' ∈ NEF(S), dann:
(i) {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)} ist ein NE-geschlossener Abschnitt in
S',
(ii) VERS(S)∖VERS(S') ⊂ {(j, Sj) | ma∖(Dom(VANS(⅛))) ≤ j < Dom(S)},
(iii) VERS(S') = (VERS(S)∖{(j, Sj) | max(Dom(VANS(S))) ≤ j < Dom(S)}) ∪
{(Dom(S), S'Dom(S))},
(iv) VANS(S)∖VANS(S') = {(max(Dom(VANS(S))), s'. .. . )},
(v) VANS(.) = 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')iDom(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') = A(Smax(Dom(VANS(S)))) ∙
Beweis: Sei S ∈ SEQ und S' ∈ NEF(S)∙ Dann gilt mit Definition 3-18 S' ∈ RGF(S)∙
Sodann gilt mit Definition 3-10: Es gibt Δ, Γ ∈ GFORM und i, j ∈ Dom(S), so dass i ≤ j,
A(Si) = Δ und (i, Si) ∈ VANS(S), A(Sj) = Γ und A(Sdo.(s)-i) = ` ɪ oder A(Sj) =
r—Γ^l und A(SDom(S)-I) = Γ und (j, Sj) ∈ VERS(S) und es gibt kein l mit i < l ≤
Dom(S)-I, so dass (l, Sl) ∈ VANS(S), und S' = S и {(Dom(S), rAlso — Δ^l)} und somit
S' ∈ SEQ und S'ΓDom(S')-1 = STDom(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'j) = Γ und A(S'Dom(s>i) = r—Γ oder A(S'j) = r—Γ und
A(S'Dom(s)-ι) = Γ und (j, S'j) ∈ VERS(STDom(S)) und es gibt kein l mit i < l ≤
Dom(S)-I, so dass (l, S'l) ∈ VANS(S'ΓDom(S)) und A(S'Dom(S)) = r—Δ^l. Damit gilt mit
Theorem 2-92, dass ® ein NE-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(S'ΓDom(S')-1)∖VANS(S') = {(min(Dom(Φ)), S min(Dom(Φ)))}
{(max(Dom(VANS(S'ΓDom(S')-1))), S max(Dom(VANS(S'fDom(S')-1))))}∙ Da S S TDom(S )-1
folgt daraus: VANS(S)∖VANS(S') = {(min(Dom(S)), S min(Dom(Φ)))}
{(max(Dom(VANS(S))), S'max(Dom(VANS(s))))} ∙ Damit ist i = min(Dom(Φ)) =