4.1 Vorbereitungen 179
TT(A(S*j)) und A(S*j) = [β*, β, A(Sj)] dann aber β ∈ TT(A(^j∙)). Sodann ergibt sich mit
a) und b) aus j ∈ Dom(VANS(S*)), dass j ∈ Dom(VANS(STDom(S)-1)) und somit
A(Sj) ∈ VAN(STDom(S)-1). Damit ware aber β ∈ TTFM(VAN(STDom(S)-1)) und an-
dererseits nach Voraussetzung β = β+ ∉ TTFM(VAN(STDom(S)-1)). Widerspruch! Also
ist β* ∉ TTFM({Δ} ∪ VAN(S*)). Da sodann A(S*i) = [β*, ζ, Δ], i ∈ Dom(VERS(S*))
und K(S+) = rΛζΔ^l ist damit dann insgesamt S+ ∈ UEF(S*).
Zweiter Fall: Sei nun β+ ≠ β. Dann lassen sich mit β+ ≠ β* und β+ = β* zwei Unterfalle
unterscheiden. Erster Unterfall: Sei β+ ≠ β*. Dann ist mit Theorem 1-25-(ii) und β+ ≠ β:
A(S*i) = [β*, β, [β+, ζ, Δ]] = [β+, ζ, [β*, β, Δ]]. Sodann ist K(S+) = rΛζ[β*, β, ΔΓ. Ange-
nommen β+ ∈ TTFM({[β*, β, Δ]} ∪ VAN(S*)). Da β+ ≠ β* und β+ ∉ TT(Δ) ist zunachst
β+ ∉ TT([β*, β, Δ]). Also ware β+ ∈ TTFM(VAN(S*)) und somit gabe es mit Definition
2-31 ein j ∈ Dom(VANS(S*)), so dass β+ ∈ TT(A(S*j)). Da mit b) A(S*j) = [β*, β,
A(Sj)] und β+ ≠ β*, ware damit aber bereits β+ ∈ TT(A(Sj)). Mit a) und b) ergabe sich
sodann aus j ∈ Dom(VANS(S*)), dass j ∈ Dom(VANS(STDom(S)-I)) und somit A(Sj)
∈ VAN(STDom(S)-I)) und damit β+ ∈ TTFM(VAN(STDom(S)-1)) und andererseits
nach Voraussetzung β+ ∉ TTFM(VAN(STDom(S)-I)). Widerspruch! Also ist β+ ∉
TTFM({[β*, β, Δ]} ∪ VAN(S*)) und damit wiederum insgesamt S+ ∈ UEF(S*).
Zweiter Unterfall: Sei nun β+ = β*. Dann ist ζ ∉ FV(Δ), da sonst β* ∈ TT([β+, ζ, Δ]) ⊆
TTSEQ(S). Damit ist dann [β+, ζ, Δ] = Δ und damit A(S*i) = [β*, β, [β+, ζ, Δ]] = [β*, β,
Δ] und sodann ist K(S+) = rΛζ[β*, β, Δ]^l. Sei nun в§ ∈ PAR∖TTSEQ(S*). Dann ist mit ζ
∉ FV(Δ) auch ζ ∉ FV([β*, β, Δ]) und damit A(S*i) = [β*, β, Δ] = [βδ, ζ, [β*, β, Δ]] und
es gilt: в§ ∉ TTFM({[β*, β, Δ]} ∪ VAN(S*)) und damit wiederum insgesamt S+ ∈
UEF(S*). Damit gilt in beiden Unterfallen und somit insgesamt in beiden Fallen, dass S+
∈ UEF(S*) ⊆ RGS.
(UBF): Sei nun S ∈ UBF(STDom(S)-I). Dann gibt es nach Definition 3-13 θ ∈
GTERM, ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass rΛζΔπ ∈
VER(STDom(S)-I), und S = STDom(S)-I ∪ {(Dom(S)-1, rAlso [θ, ζ, Δ]π)}. Mit d) ist
dann S+ = S* ∪ {(Dom(S)-1, [β*, β, rAlso [θ, ζ, Δ]π])} = S* ∪ {(Dom(S)-1, rAlso [β*,
β, [θ, ζ, Δ]]^l)}. Sodann gibt es mit rΛζΔ^l ∈ VER(STDom(S)-1) nach Definition 2-30 i ∈
Dom(VERS(STDom(S)-1)), so dass A(Si) = rΛζΔ^l. Mit a) und b) ist dann i ∈
Dom(VERS(S*)) und A(S*i) = [β*, β, rΛζΔ^l ] = rΛζ[β*, β, Δ]^l. Sodann ist mit Theorem
1-26-(ii) K(S+) = [β*, β, [θ, ζ, Δ]] = [[β*, β, θ], ζ, [β*, β, Δ]], wobei mit θ ∈ GTERM