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, .,
More intriguing information
1. Should Local Public Employment Services be Merged with the Local Social Benefit Administrations?2. Understanding the (relative) fall and rise of construction wages
3. The name is absent
4. Declining Discount Rates: Evidence from the UK
5. The name is absent
6. The name is absent
7. The name is absent
8. The name is absent
9. Design and investigation of scalable multicast recursive protocols for wired and wireless ad hoc networks
10. The name is absent