258 6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls
BelegungsvariantenH von bX fur DX sind: DX, IX, b' ⅛ [β, ξ, Δ]. Nach Theorem 5-8H-(i)
gilt somit DX, IX, bX =h rΛξΔ^l = Γ.
Siebtens: Sei Γ = rVξΔ^l. Dann gibt es mit Definition 6-2-(xiii) ein θ ∈ GTERMH, so
dass [θ, ξ, Δ] ∈ X. Nach Theorem 1-13H ist dann FGRADH([θ, ξ, Δ]) < FGRADH(Γ) und
damit gilt nach I.V. DX, IX, bX ⅛ [θ, ξ, Δ]. Sei nun β ∉ TTH(Δ). Sei nun b' = (bX∖{(β,
bX(β))} ∪ {(β, [θ]A)}. Dann ist b' in β eine BelegungsvarianteH von bX fur DX mit b'(β) =
[θ]A. Sodann ist TDH(θ, DX, IX, bX) = [θ]A und somit b'(β) = TDH(θ, DX, IX, bX). Wegen DX,
IX, bX ⅛ [θ, ξ, Δ] folgt dann mit Theorem 5-9H-(ii): DX, IX, b` ⅛ [β, ξ, Δ]. Also gibt es
ein b', das in β BelegungsvarianteH von bX fur DX ist, so dass DX, IX, b` =n [β, ξ, Δ]. Nach
Theorem 5-8H-(ii) gilt somit DX, IX, bX ⅛ rVξΔ^l = Γ.
Nun wird gezeigt: Wenn r—Γ^l ∈ X, dann DX, IX, bX ≠∣∣ Γ. Sei nun r—Γ ∈ X. Nach
Annahme ist 0 < FGRADH(Γ). Damit konnen sieben Falle unterschieden werden. Erstens:
Sei Γ = r—B^l. Dann ist mit Definition 6-2-(ii) Β ∈ X und weil FGRADH(B) <
FGRADH(Γ) gilt nach I.V. DX, IX, bX =n B. Mit Theorem 5-4H-(ii) folgt DX, IX, bX ≠n
r—B^l = Γ. Zweitens: Sei Γ = rΑ ∧ B^l. Dann ist mit Definition 6-2-(iv) r—Α^l ∈ X oder
r-Bπ ∈ X und weil FGRADH(A) < FGRADH(Γ) und FGRADH(B) < FGRADH(Γ) gilt
nach I.V. DX, IX, bX ≠n A oder DX, IX, bX ≠n B. Mit Theorem 5-4H-(iii) folgt DX, IX, bX ≠n
rA ∧ B^l = Γ. Der dritte bis funfte Fall verlaufen analog.
Sechstens: Sei Γ = r-ΛξΔ^l. Dann gilt mit Definition 6-2-(xii): Es gibt ein θ ∈
GTERMH, so dass —[θ, ξ, Δ] ∈ X. Nach Theorem 1-13H gilt dann FGRADH([θ, ξ, Δ]) <
FGRADH(Γ). Damit gilt nach I.V.: DX, IX, bX ≠n [θ, ξ, Δ]. Sei nun β ∉ TTH(Δ). Sei nun b'
in β die BelegungsvarianteH von bX fur DX mit b'(β) = [θ]A. Dann ist TDH(θ, DX, IX, bX) =
[θ]A und somit b,(β) = TDH(θ, DX, IX, bX). Wegen DX, IX, bX ≠∏ [θ, ξ, Δ] folgt dann mit
Theorem 5-9H-(ii): DX, IX, b' ≠n [β, ξ, Δ]. Also gibt es ein bl, das in β BelegungsvarianteH
von bX fur DX ist, so dass DX, IX, b' ≠∣∣ [β, ξ, Δ]. Somit gilt mit Theorem 5-8H-(i) DX, IX, bX
^H " - \ .
Siebtens: Sei Γ = r-VξΔ^l. Dann gilt mit Definition 6-2-(xiv) fur alle θ ∈ GTERMH
r—[θ, ξ, Δ]^l ∈ X. Da fur alle θ ∈ GTERMH nach Theorem 1-13H FGRADH([θ, ξ, Δ]) <
FGRADH(Γ), gilt damit nach I.V. fur alle θ ∈ GTERMH: DX, IX, bX ≠∏ [θ, ξ, Δ]. Sei nun β