4.1 Vorbereitungen 187
sodann aus j ∈ Dom(VANS(ft*)), dass j-1 ∈ Dom(VANS(ftΓDom(ft)-1)) und somit
A(ftj-ι) ∈ VAN(ftΓDom(ft)-1) und β* ∈ TTFM(VAN(ftΓDom(ft)-1)) und andererseits
nach Voraussetzung β* ∉ TTFM(VΛN(ftfDom(ft)-1)). Widerspruch! Also ist β* ∉
TTFM({[β, α, Δ]} ∪ VAN(ft*)) und damit ft+ ∈ UEF(ft*).
Zweiter Fall: Sei nun β* = β. Dann ist ζ ∉ FV(Δ), da sonst β ∈ TT([β*, ζ, Δ]) ⊆
TTSEQ(ft). Damit ist dann [β*, ζ, Δ] = Δ und damit A(ft*i+ι) = [β, α, [β*, ζ, Δ]] = [β, α,
Δ] und sodann ist K(ft+) = rΛζ[β, α, Δ]^l. Sei nun β+ ∈ PAR∖TTSEQ(ft*). Dann ist mit ζ
∉ FV(Δ) auch ζ ∉ FV([β, α, Δ]) und damit A(ft*i+ι) = [β, α, Δ] = [β+, ζ, [β, α, Δ]] und es
gilt: β+ ∉ TTFM({[β, α, Δ]} ∪ VAN(ft*)) und damit wiederum ft+ ∈ UEF(ft*). Damit
gilt in beiden Fallen, dass ft+ ∈ UEF(ft*) ⊆ RGS.
(UBF): Sei nun ft ∈ UBF(ftΓDom(ft)-1). Nach Definition 3-13 gibt es dann θ ∈
GTERM, ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass rΛζΔπ ∈
VER(ftΓDom(ft)-1) und ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso [θ, ζ, Δ]^l)}. Mit f) ist
dann ft+ = ft* ∪ {(Dom(ft), [β, α, rAlso [θ, ζ, Δ]^l])} = ft* ∪ {(Dom(ft), rAlso [β, α, [θ,
ζ, Δ]]^l)}. Sodann gibt es mit rΛζΔ^l ∈ VER(ftΓDom(ft)-1) nach Definition 2-30 ein i ∈
Dom(VERS(ftΓDom(ft)-1)), so dass A(fti) = rΛζΔ^l. Mit c) und d) ist dann i+1 ∈
Dom(VERS(ft*)) und A(ft*i+ι) = [β, α, rΛζΔπ] = rΛζ[β, α, Δ]^l. Sodann ist mit Theorem
1-26-(ii) K(ft+) = [β, α, [θ, ζ, Δ]] = [[β, α, θ], ζ, [β, α, Δ]], wobei mit θ ∈ GTERM auch
[β, α, θ] ∈ GTERM und mit FV(Δ) ⊆ {ζ} auch FV([β, α, Δ]) ⊆ {ζ}. Damit ist dann ins-
gesamt ft+ ∈ UBF(ft*) ⊆ RGS.
(PEF): Sei nun ft ∈ PEF(ftΓDom(ft)-1). Nach Definition 3-14 gibt es dann θ ∈
GTERM, ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass [θ, ζ, Δ] ∈
VER(ftΓDom(ft)-1) und ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso VζΔ^l)}. Mit f) ist dann
ft+ = ft* ∪ {(Dom(ft), [β, α, rAlso VζΔ^l])} = ft* ∪ {(Dom(ft), rAlso Vζ[β, α, Δ]^l)}. So-
dann gibt es mit [θ, ζ, Δ] ∈ VER(ftΓDom(ft)-1) nach Definition 2-30 ein i ∈
Dom(VERS(ftΓDom(ft)-1)), so dass A(fti) = [θ, ζ, Δ]. Mit c) und d) ist dann i+1 ∈
Dom(VERS(ft*)) und A(ft*i+ι) = [β, α, A(fti)]. Dann ist mit Theorem 1-26-(ii) A(ft*i+ι)
= [β, α, A(fti)] = [β, α, [θ, ζ, Δ]] = [[β, α, θ], ζ, [β, α, Δ]], wobei mit θ ∈ GTERM auch [β,
α, θ] ∈ GTERM und mit FV(Δ) ⊆ {ζ} auch FV([β, α, Δ]) ⊆ {ζ}. Damit ist dann insge-
samt ft+ ∈ PEF(ft*) ⊆ RGS.
(IEF): Sei nun ft ∈ IEF(ftΓDom(ft)-1). Nach Definition 3-16 gibt es dann θ ∈ GTERM,
so dass ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso θ = θ^l)}. Dann ist mit f) ft+ = ft* ∪