36 1 Zum grammatischen Rahmen
Theorem 1-22. Eindeutige Substitutionsorte (b) fur Terme
Wenn θ, θ+ ∈ TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ+)), ξ ∈ VAR, β ∈ PAR und [θ*, ξ, θ] =
[θ*, β, θ+], dann θ+ = [β, ξ, θ].
Beweis: Durch Induktion uber den Termaufbau von θ. Sei θ ∈ ATERM. Sei nun θ+ ∈
TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ+)), ξ ∈ VAR, β ∈ PAR und [θ*, ξ, θ] = [θ*, β, θ+].
Dann ist θ ∈ KONST ∪ PAR ∪ VAR. Sei nun θ ∈ KONST. Dann ist [θ*, ξ, θ] = θ. Dann
ist θ = [θ*, β, θ+], womit sich wegen θ* ∉ TT(θ) und Theorem 1-14-(i) ergibt, dass θ = θ+
und wegen θ ≠ ξ: θ+ = θ = [β, ξ, θ]. Sei nun θ ∈ PAR. Dann ist [θ*, ξ, θ] = θ. Dann ist θ =
[θ*, β, θ+], womit sich wegen θ* ∉ TT(θ) und Theorem 1-14-(i) ergibt, dass auch θ = θ+
und wegen ξ ≠ θ: θ+ = θ = [β, ξ, θ]. Sei nun θ ∈ VAR. Angenommen θ = ξ. Dann ist [θ*,
ξ, θ] = θ*. Dann ist θ* = [θ*, β, θ+]. Dann ist wegen θ* ≠ θ+ β ∈ TT(θ+). Damit ist θ* ∈
TT([θ*, β, θ+]). Ware nun θ+ ≠ β ergabe sich dann mit θ* = [θ*, β, θ+], dass θ* im Wider-
spruch zu Theorem 1-8 echter Teilterm von sich selbst ware. Also gilt θ+ = β = [β, ξ, θ].
Sei nun θ ≠ ξ. Dann ist θ = [θ*, ξ, θ]. Dann ist θ = [θ*, β, θ+]. Dann ist wegen θ* ∉ TT(θ)
und Theorem 1-14-(i) θ = θ+ und wegen θ ≠ ξ: θ+ = θ = [β, ξ, θ].
Gelte die Behauptung nun fur {θ0, ..., θr-ι} ⊆ TERM und sei rφ(θ0, ..., θr-1)^l ∈
FTERM. Sei nun θ+ ∈ TERM, θ* ∈ TERM∖(TT( rφ(θo, ., θr-ʃ) ∪ TT(θ+)), ξ ∈ VAR, β
∈ PAR und [θ*, ξ, rφ(θo, ., = [θ*, β, θ+]. Also [θ*, β, θ+] = rφ([θ*, ξ, θo], ., [θ*,
ξ, θr-ι])^l ∈ FTERM. Ware θ+ ∈ ATERM. Dann ware β ≠ θ+ oder β = θ+. Angenommen β
≠ θ+. Dann ist θ+ = [θ*, β, θ+] = rφ([θ*, ξ, θo], ., [θ*, ξ, θr-ι])π ∈ FTERM. Widerspruch!
Angenommen β = θ+. Dann ist θ* = [θ*, β, θ+] = rφ([θ*, ξ, θ0], ., [θ*, ξ, θr-1])^l. Mit
Theorem 1-14-(i) gilt dann fur alle i < r: [θ*, ξ, θi] = θi oder es gibt ein i < r, so dass θ* ∈
TT([θ*, ξ, θi]). Wenn [θ*, ξ, θi] = θi fur alle i < r, dann θ* = rφ([θ*, ξ, θo], ., [θ*, ξ,
θr-1])^l = rφ(θ0, ., θr-ι)^l und damit entgegen der Voraussetzung θ* ∈ TT(rφ(θ0, .
θr-1)^l). Wenn es andererseits ein i < r gibt, so dass θ* ∈ TT([θ*, ξ, θi]), dann ist θ* echter
Teilterm von rφ([θ*, ξ, θ0], ., [θ*, ξ, θr-1])^l, also echter Teilterm von sich selbst. Wider-
spruch zu Theorem 1-8. Also θ+ ∉ ATERM, sondern θ+ ∈ FTERM. Also gibt es {θ'o, .,
θ'k-ι} ⊆ TERM und φ' ∈ FUNK, so dass θ+ = rφ'(θ'o, ., θ'k-ι)π. Damit ist rφ'([θ*, β, θ'o],
., [θ*, β, θ'k-ι])π = [θ*, β, rφ'(θ'o, ., θ'k-ʃ] = [θ*, β, θ+] = rφ([θ*, ξ, θo], ., [θ*, ξ,
θr-ι])^l. Mit Theorem 1-11-(ii) gilt dann k = r und φ' = φ und [θ*, β, θ'i] = [θ*, ξ, θi] fur al-
le i < r. Mit I.V. ergibt sich, dass θ'i = [β, ξ, θi] fur alle i < r. Damit ist dann θ+ = rφ'(θ'0,
., θ'k-ι)π = rφ([β, ξ, θo], ., [β, ξ, θr-1])π = [β, ξ, rφ(θo, ., θr-ʃ]. ■