3.3 VERS, VANS, VER und VAN in Ableitungen und bei einzelnen Ubergangen 147
A(A‘Dom(A)) = Γ. Damit gilt mit Theorem 2-93, dass ® ein PB-geschlossener und damit
auch ein geschlossener Abschnitt in A' ist.
Da sodann max(Dom(Φ)) = Dom(A) = Dom(A')-1, ergibt sich mit Theorem 2-86,
dass VANS(A'TDom(A')-1)∖VANS(A') = {(min(Dom(Φ)), A min(Dom(Φ)))}
{(max(Dom(VANS(A'TDom(A')-1))), A max(Dom(VANS(A'TDom(A')-1))))}. Da A A fDom(^ )-1
folgt daraus: VANS(A)∖VANS(A') = {(min(Dom(Φ)), A min(Dom(!B)))}
{(max(Dom(VANS(A))), A'max(i>o,,,,∙vans(a)))) }. Damit ist i = min(Dom(Φ)) =
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 K(A) = A(A'Dom(A)-ι) = Γ = K(A') und somit gilt
(x). Sodann ergibt sich mit VANS(A)∖VANS(A') ≠ 0 und Theorem 2-73 auch
VERS(A)∖VERS(A') ≠ 0. Damit und mit A = ATDom(A)-I 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-22. Ist die zuletzt angenommene Aussage nur einmal als Annahme verfugbar,
dann wird sie bei SE, NE undPB eliminiert
Wenn A ∈ SEQ, Δ ∈ GFORM und fur alle i ∈ Dom(VANS(A)) gilt: Wenn A(Ai) = Δ, dann i
= max(Dom(VANS(A))), dann gilt fur alle A' ∈ SEF(A) ∪ NEF(A) ∪ PBF(A): VAN(A) ⊆
VAN(A)∖{Δ}.
Beweis: Sei A ∈ SEQ, Δ ∈ GFORM und gelte fur alle i ∈ Dom(VANS(A)): Wenn A(Ai)
= Δ, dann i = max(Dom(VANS(A))). Sei nun A' ∈ SEF(A) ∪ NEF(A) ∪ PBF(A). Dann
gilt mit Theorem 3-19-(iv), -(v), Theorem 3-20-(iv), -(v) und Theorem 3-21-(iv), -(v),
dass VANS(A)∖VANS(A') = {(max(Dom(V ANS(A))), A'max(Dom(VANS(A))))} und
VANS(A') ⊆ VANS(A). Mit Theorem 2-75 gilt VAN(A') ⊆ VAN(A).
Damit gilt: Δ ∉ VAN(A'). Ware namlich Δ ∈ VAN(A'). Dann gabe es nach Definition
2-31 i ∈ Dom(VANS(A')), so dass Δ = A(A'i). Dann gilt mit VANS(A') ⊆ VANS(A),
dass i ∈ Dom(VANS(A)) und es ist Δ = A(Ai). Da nun nach Annahme fur alle i ∈
Dom(VANS(A)) gilt: Wenn A(Ai) = Δ, dann i = max(Dom(V ANS(A))) ware damit
max(Dom(VANS(A))) = i ∈ Dom(VANS(A')). Mit VANS(A)∖VANS(A') =
{(max(Dom(VANS(A))), A'max(Dom(VANS(A))))} gilt nun jedoch max(Dom(VANS(A))) ∉
Dom(VANS(A')). Widerspruch! Also ist Δ ∉ VAN(A') und damit VAN(A') ⊆
VAN(A)∖{Δ}. ■