4.1 Vorbereitungen 185
dass dann auch ft+ ∈ NEF(ft*) ⊂ RGS und Dom(VERS(ft+)) = {(l+1 | l ∈
Dom(VERS(ft))} и {0}.
(PBF): Sei nun ft ∈ PBF(ftΓDom(ft)-1). Nach Definition 3-15 gibt es dann β* ∈ PAR,
ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊂ {ζ}, und i ∈ Dom(VERS(ftΓDom(ft)-1)), so dass
A(fti) = rVζΔπ, A(ftm) = [β*, ζ, Δ], wobei i+1 ∈ Dom(VANS(ftΓDom(ft)-1)), β* ∉
TTFM({Δ, A(∙‰om(⅛)-2)}), es kein j ≤ i gibt, so dass β* ∈ TT(ftj), es kein l mit i+1 < l ≤
Dom(ft)-2 gibt, so dass l ∈ Dom(VANS(ftΓDom(ft)-1)), und ft = ftΓDom(ft)-1 и
{(Dom(ft)-1, rAlso AWO-
Damit ergibt sich dann mit c), d) und f) zunachst: i+1 ∈ Dom(VERS(ft*)) und A(ft*i+ι)
= [β, α, A(fti)] = [β, α, rVζΔπ] = rVζ[β, α, Δ]∖ i+2 ∈ Dom(VANS(ft*)) und A(ft‰) =
[β, α, A(‰)] = [β, α, [β*, ζ, Δ]], K(ft*) = A(ft*Dom№)-1) = [β, α, A‰m(ft)-2)] und ft+ =
ft* и {(Dom(ft), [β, α, rAlso K(ftΓDom(ft)-1)^l])} = ^* и {(Dom(ft), rAlso [β, α,
K(ftΓDom(ft)-1)]^l)} = ft* и {(Dom(ft), rAlso K(ft*f)} und es gibt kein l mit i+2 < l ≤
Dom(ft)-1 = Dom(ft*)-1, so dass l ∈ Dom(VANS(ft*)). Sodann lassen sich mit β* ≠ β
und β* = β zwei Falle unterscheiden.
Erster Fall: Sei β* ≠ β. Dann ist mit Theorem 1-25-(ii) A(ft*i+2) = [β, α, [β*, ζ, Δ]] =
[β*, ζ, [β, α, Δ]]. Sodann ist A(ft*i+1) = rVζ[β, α, Δ]π. Ware nun β* ∈ TTFM({[β, α, Δ],
[β, α, A(^D0m(⅛)-2)]}) oder gabe es ein j ≤ i+1, so dass β* ∈ TT(ft*j), dann ware wegen β*
≠ β mit d) auch β* ∈ TTFM({Δ, A(ftDom(ft)-2)}) oder es gabe j ≤ i, so dass β* ∈ TT(ftj).
Widerspruch! Also ist β* ∉ TTFM({[β, α, Δ], [β, α, A(ftDom(ft)-2)]}) und es gibt kein j ≤
i+1, so dass β* ∈ TT(ft*j) und damit ist ft+ ∈ PBF(ft*) und damit ft+ ∈ RGS.
Zweiter Fall: Sei nun β* = β. Dann ist ζ ∉ FV(Δ), da sonst β ∈ TT([β*, ζ, Δ]) ⊂
TTSEQ(ft). Dann ist [β*, ζ, Δ] = Δ und damit A(ft*2) = [β, α, [β*, ζ, Δ]] = [β, α, Δ] und
sodann ist A(ft*i+ι) = rVζ[β, α, Δ]^l. Sei nun β+ ∈ PAR∖TTSEQ(ft*). Dann ist mit ζ ∉
FV(Δ) auch ζ ∉ FV([β, α, Δ]) und damit A(ft*2) = [β, α, Δ] = [β+, ζ, [β, α, Δ]] und es
gilt: β+ ∉ TTFM({[β, α, Δ], [β, α, A(‰m(⅛)-2)]}) und es gibt kein j ≤ i+1, so dass β+ ∈
TT(ft*j). Damit ist dann wieder ft+ ∈ PBF(ft*) und damit ft+ ∈ RGS. Damit gilt in bei-
den Fallen ft+ ∈ PBF(ft*) und damit ft+ ∈ RGS.
Sodann ergibt sich mit Theorem 3-21-(iii), dass VERS(ft) = VERS(ftΓDom(ft)-1)∖{(j,
ftj) | i+1 ≤ j < Dom(ft)-1} и {(Dom(ft)-1, rAlso A(ftDom(ft)-2)^l)} und dass VERS(ft+) =
VERS(ft*)∖{(j, ft) | i+2 ≤ j < Dom(ft)} и {(Dom(ft), rAlso [β, α, A‰m^2)Γ)}. Mit
Dom(VERS(ft*)) = {(l+1 | l ∈ Dom(VERS(ftΓDom(ft)-1))} и {0} ergibt sich dann wie-
der Dom(VERS(ft+)) = {(l+1 | l ∈ Dom(VERS(ft))} и {0}.