4.1 Vorbereitungen 191
a) Dom(ft*) = Dom(ft')+k,
b) ft*[^Dom(ft') = ft'
c) VAN(ft*) ⊆ VAN(ft'),
d) Fur alle i < k-1: K(ft*fDom(ft')+i+1) = rΛζi+1.Λζk.1[<θ'o, ., θ'i>, <ζo, ., ζi>, [θo,
ξo, Δ]]^, und
e) K(ft*) = [<θ'o, ., θ'fc-ι>, <ζo, ., ζk-1>, [θo, ξo, Δ]].
Dann ergibt sich mit a) wegen Dom(ft') = Dom(ft)+1: Dom(ft*) = Dom(ft)+k+1. Sodann
ergibt sich mit b) wegen ft'ΓDom(ft) = ft auch ft*ΓDom(ft) = ft. Mit c) ergibt sich wegen
VAN(ft') ⊆ VAN(ft), dass VAN(ft*) ⊆ VAN(ft). Damit gilt bereits, dass ft* ∈
RGS∖{0} und dass die Klauseln (i) bis (iii) fur ft* gelten. Aus d) ergibt sich sodann mit ζi
= ξi+1 und θ'i = θi+1:
Fur alle i < k-1: K(ft*fDom(ft')+i+1) = rΛξi+2 ... Λξk[<θ1, ., θi+1>, <ξι, ., ξ+ι>, [θo, ξo,
∆]Γ.
Mit Dom(ft') = Dom(ft)+1 gilt damit:
f) Fur alle i < k-1: K(ft*fDom(ft)+i+1+1) = rΛξi+2 . Λξfc[<θ1, ., θi+1>, <ξ1, ., ξi+1>, [θo,
ξo, Δ]Γ.
Damit gilt:
g) Fur alle i mit o < i < k: K(ft*[^Dom(ft)+i+1) = rΛξi+1 . Λξk[<θ1, ., θi>, <ξb ., ξi>, [θo,
ξo, Δ]Γ.
Sodann gilt:
h) Fur alle i mit o < i < k+1: [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]] = [<θo, ., θi>, <ξo, ., ξi>,
Δ].
h) kann mittels Induktion uber i gezeigt werden. Es gilt namlich zunachst mit Theorem
1-28-(ii), dass [θ1, ξ1, [θo, ξo, Δ]] = [<θo, θ1>, <ξo, ξ1>, Δ]. Gelte nun fur i: Wenn o < i < k+1,
dann [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]] = [<θo, ., θi>, <ξo, ., ξi>, Δ]. Sei nun o < i+1 <
k+1. Dann ist i = o oder o < i. Fur i = o ergibt sich die Behauptung wie fur die Indukti-
onsbasis. Sei nun o < i. Dann ergibt sich zunachst wieder mit Theorem 1-28-(ii): [<θ1, .,
θi+1>, <ξ1, ., ξi+1>, [θo, ξo, Δ]] = [θi+1, ξi+1, [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]]]. Mit I.V. gilt
dann [θi+1, ξi+1, [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]]] = [θi+1, ξi+1, [<θo, ., θi>, <ξo, ., ξi>, Δ]]
und wiederum mit Theorem 1-28-(ii): [θi+1, ξi+1, [<θo, ., θi>, <ξo, ., ξi>, Δ]] = [<θo, .,