192 4 Theoreme zur deduktiven Konsequenzschaft
θi+ι>, <ξo, ., ξi+ι>, Δ] und damit insgesamt: [<θι, ..., θi+ι>, <ξι, ..., ξi+1), [θo, ξo, Δ]] = [<θo,
., θi+ι>, <ξo, ., ξi+ι>, Δ]. Also gilt h).
Sodann gilt mit Dom(S') = Dom(S)+1 und K(S*ΓDom(S')) = K(S') = rΛξ1 ... Λξk[θ0,
ξ0, Δ]^l, dass K(S*ΓDom(S)+0+1) = rΛξ1 .. Λξk[θ0, ξ0, Δ]^l. Mit g) und h) gilt dann ins-
gesamt Klausel (iv):
Fur alle i < k: K(S*fDom(S)+i+1) = rΛξ,w . Λξk[<θo, ., θ.,), <ξo, ., ξ>, ΔJ1.
Zuletzt gilt mit e), h) und θ'i = θi+1 und ζi = ξi+1:
K(S*) = [<θ'o, ., θ'k-i>, <ζo, ., ζk-i>, [θo, ξo, Δ]]
[<θ1, ., θk>, <ξ1, ., ξk>, [θo, ξo, Δ]]
[<θo, ., θk>, <ξo, ., ξk>, Δ]
und damit Klausel (v), womit insgesamt das Theorem fur k+1 gilt. ■
Theorem 4-13. Induktionsbasis fur Theorem 4-14
Wenn S, S' ∈ RGS∖{0} und VANS(S') = 0, dann gibt es ein S* ∈ RGS∖{0}, so dass
(i) K(S), K(S') ∈ VER(S*) und
(ii) VAN(S*) ⊆ VAN(S).
Beweis: Seien S, S ∈ RGS∖{0} und sei VANS(S') = 0. Wenn K(S) = K(S'), konnen so-
wohl S als auch S' fur S* gewahlt werden. Sei nun K(S) ≠ K(S'). Dann lassen sich mit
PAR ∩ TTSEQ(S) ∩ TTSEQ(S') = 0 und PAR ∩ TTSEQ(S) ∩ TTSEQ(S') ≠ 0 zwei
Falle unterscheiden.
Erster Fall: Sei PAR ∩ TTSEQ(S) ∩ TTSEQ(S') = 0. Nun gibt es ein α ∈
KONST∖(TTSEQ(S) ∪ TTSEQ(S')). Dann gibt es mit Theorem 4-4 ein S+ ∈ RGS∖{0},
so dass VER(S) ∪ VER(S') ⊆ VER(S+) und VAN(S+) = VAN(S) ∪ {rα = α^l} ∪
VAN(S'). Nun ist mit Theorem 2-82 K(S) ∈ VER(S) und K(S') ∈ VER(S') und damit
sind dann K(S), K(S') ∈ VER(S+). Sodann gibt es mit Theorem 4-7 S* ∈ RGS∖{0}, so
dass VAN(S*) ⊆ VAN(S+)∖{ rα = α^l} = (VAN(S) ∪ {rα = α^l} ∪ VAN(S'))∖{ rα = α^l}
⊆ VAN(S) ∪ VAN(S') und K(S), K(S') ∈ VER(S*), womit S* das gesuchte RGS-
Element ist.
Zweiter Fall: Sei nun PAR ∩ TTSEQ(S) ∩ TTSEQ(S') ≠ 0. Dann kommen in S' k
paarweise verschiedene Parameter fur ein k ∈ N\{o} vor. Sei nun {βo, ., βk-1} = PAR ∩