4.1 Vorbereitungen 189
Theorem 4-11. UE-Fortsetzung einer Sequenz
Wenn Q ∈ RGS∖{0}, k ∈ N∖{0}, {ξo, ., ξk-ι} ⊆ VAR, wobei fur alle i, j < k mit i ≠ j gilt: ξi
≠ ξj, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξo, ., ξk-ι}, und {βo, ... βk-1} ⊆ PAR∖TTFM({Δ} ∪
VAN(Q)), wobei fur alle i, j < k mit i ≠ j gilt: βi ≠ βj, und K(Q) = [<βo, ., βk-1>, <ξo, ., ξ⅛-ι>,
Δ], dann gibt es ein Q* ∈ RGS∖{0}, so dass
(i) PAR ∩ TTSEQ(Q*) = PAR ∩ TTSEQ(Q),
(ii) VAN(Q*) ⊆ VAN(Q) und
(iii) K(Q*) = 'ξ.'ξ Δ'.
Beweis: Durch Induktion uber k. Sei k = 1 und Q ∈ RGS∖{0}, sei ξ ∈ VAR, Δ ∈ FORM,
wobei FV(Δ) ⊆ {ξ} und β ∈ PAR∖TTFM({Δ} ∪ VAN(Q)) und K(Q) = [β, ξ, Δ]. Da dann
mit Theorem 2-82 [β, ξ, Δ] = K(Q) ∈ VER(Q), ist nach Definition 3-12 Q* = Q ∪
{(Dom(Q), rAlso ΛξΔ^l) ∈ UEF(Q) ⊆ RGS∖{0} und K(Q*) = rΛξΔ^l. Sodann ist PAR ∩
TTSEQ(Q*) = (PAR ∩ TTSEQ(Q)) ∪ (PAR ∩ TT(rΛξΔπ)) = PAR ∩ TTSEQ(Q) und mit
Theorem 3-26-(v) ist VAN(Q*) ⊆ VAN(Q).
Gelte die Behauptung nun fur k und sei Q ∈ RGS∖{0}, {ξ0, ., ξk} ⊆ VAR, wobei fur i,
j < k+1 mit i ≠ j gelte: ξi ≠ ξj, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξo, ., ξk} und {βo, . βk} ⊆
PAR∖TTFM({Δ} ∪ VAN(Q)), wobei fur i, j < k+1 mit i ≠ j gelte: βi ≠ βj, und K(Q) =
[<βo, ., βfc>, <ξo, ., ξfc>, Δ]. Mit Theorem 1-28-(ii) ist dann K(Q) = [<βo, ., βfc>, <ξo, .,
ξk>, Δ] = [βk, ξk, [<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]]. Mit FV(Δ) ⊆ {ξo, ., ξk} ist dann
FV<[<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]) ⊆ {ξk} und mit der paarweisen Verschiedenheit der βi
und {βo, . β⅛} ⊆ PAR∖TTFM({Δ} ∪ VAN(Q)) ist dann βfc ∈ PAR∖TTFM({[<βo, .,
βk-1>, <ξo, ., ξfc-1>, Δ]} ∪ VAN(Q)). Da sodann [βfc, ξfc, [<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]] =
K(Q) ∈ VER(Q) ist nach Definition 3-12 Q' = Q ∪ {(Dom(Q), rAlso Λξk[<βo, ., βk-1>,
<ξo, ., ξk-1>, ΔJ1) ∈ UEF(Q) ⊆ RGS∖{0} und K(Q') = rΛξk[<βo, ., βk-1>, <ξo, ., ξk-1>, ΔJ1
und PAR ∩ TTSEQ(Q') = (PAR ∩ TTSEQ(Q)) ∪ (PAR ∩ TT(rΛξk[<βo, ., βk-1>, <ξo, .,
ξk-1>, Δ]^l)) = PAR ∩ TTSEQ(Q) und mit Theorem 3-26-(v) ist VAN(Q') ⊆ VAN(Q).
Wegen der paarweisen Verschiedenheit der ξi ist sodann fur alle i < k: ξi ≠ ξk. Damit ist
dann K(Q) = rΛξk[<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]π = [<βo, ., βk-1>, <ξo, ., ξk-1>, rΛξkΔ1].
Mit FV(Δ) ⊆ {ξo, ., ξk} ist dann FV(rΛξkΔπ) ⊆ {ξo, ., ξk-1}, wobei die ξi mit i < k
paarweise verschieden sind. Sodann ist mit {βo, . βk} ⊆ PAR∖TTFM({Δ} ∪ VAN(Q))
dann {βo, . βk-1} ⊆ PAR∖TTFM({ rΛξkΔ^l} ∪ VAN(Q)), wobei die βi mit i < k ebenfalls
paarweise verschieden sind. Nach I.V. gibt es damit mit K(Q') = [<βo, ., βk-1>, <ξo, .,