146 3 Der Redehandlungskalkul
max(Dom(VANS(A))) und es gilt: ® = {(j, A'j) | max(Dom(VANS(A))) ≤ j ≤ Dom(A)}.
Damit gilt dann (i). Auβerdem gilt dann A(A'max(Dom(vANs( a >») = A(Ai) = Δ und da K(A') =
AV gilt dann (x). Sodann ergibt sich mit VANS(A)∖VANS(A') ≠ 0 und Theorem 2-73
auch VERS(A)WeRS(A) ≠ 0. Damit und mit A = A'ΓDom(A')-1 und ® = {(j, A'j) |
max(Dom(VANS(A))) ≤ j ≤ Dom(A)} ergeben sich dann mit Theorem 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-21. VERS, VANS, VER und VAN bei PB
Wenn A ∈ SEQ und A' ∈ PBF(A), dann:
(i) {(j, A'j) | max(Dom(VANS(A))) ≤ j ≤ Dom(A)} ist ein PB-geschlossener Abschnitt in
A',
(ii) VERS(A)∖VERS(A') ⊆ {(j, A'j) | max(Dom(VANS(A))) ≤ j < Dom(A)},
(iii) VERS(A') = (VERS(A)∖{(j, A'j) | max(Dom(VANS(A))) ≤ j < Dom(A)}) и
{(Dom(A), A Dom(A))},
(iv) VANS(A)∖VANS(A') = {(max(Dom(VANS(A))), A'max(Dom(VANS(A))))},
(v) VANS(A) = VANS(A') U {(max(Dom(VANS(A))), A'max(Dom(VANS(A))))},
(vi) VER(A)∖VER(A') ⊆ {A(A'j) | max(Dom(VANS(A))) ≤ j < Dom(A)},
(vii) VER(A) ⊆ {A(A'j) | j ∈ Dom(VERS(A')iDom(A))} и
{A(A'j) | max(Dom(VANS(A))) ≤ j < Dom(A)},
(Viii) VAN(A)∖VAN(A') ⊆ {A(A'max(Dom(VANS(A))))},
(ix) VAN(A) = VAN(A') U {A(A'max(Dom(VANS(A))))} und
(x) K(A') = K(A).
Beweis: Sei A ∈ SEQ und A' ∈ PBF(A). Dann gilt mit Definition 3-18 A' ∈ RGF(A). So-
dann gilt mit Definition 3-15: Es gibt β ∈ PAR, ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆
{ξ}, Γ ∈ GFORM und i ∈ Dom(A), so dass A(Ai) = rVξΔ^l und (i, Ai) ∈ VERS(A),
A(Ai+1) = [β, ξ, Δ] und (i+1, Ai+1) ∈ VANS(A), und A(Aυom(A)-1) = Γ, wobei β ∉
TTFM({Δ, Γ}), und es kein j ≤ i gibt, so dass β ∈ TT(Aj), und es kein m mit i+1 < m ≤
Dom(A)-1 gibt, so dass (m, Am) ∈ VANS(A), und A' = A и {(Dom(A), rAlso Γ)} und
somit A' ∈ SEQ und A'ΓDom(A')-1 = AlDom(A) = A.
Sodann ist ® = {(j, A'j) | i+1 ≤ j ≤ Dom(A)} ein Abschnitt in A' und β ∈ PAR, ξ ∈
VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ}, Γ ∈ GFORM und A(A'i) = VξΔπ und (i, A'i) ∈
VERS(A'ΓDom(A)), A(A'i+1) = [β, ξ, Δ] und (i+1, A'i+1) ∈ VANS(A'ΓDom(A)-1), und
A(A'Dom<A)-ι) = Γ, wobei β ∉ TTFM({Δ, Γ}), und es gibt kein j ≤ i, so dass β ∈ TT(A'j),
und es gibt kein m mit i+1 < m ≤ Dom(A)-1, so dass (m, A'm) ∈ VANS(AlDom(A))5 und