4.1 Vorbereitungen 167
gdw
k ∈ Dom(VERS(⅛*)) und k < Dom(⅛)+1+i oder k = Dom(⅛)+1+Dom(⅛')-1
gdw
k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ∈ {(Dom(⅛)+1+l | l ∈
Dom(VERS(⅛'[^Dom(⅛')-1))} und k < Dom(⅛)+1+i oder k = Dom(^)+1+Dom(⅛')-1
gdw
k < Dom(⅛)+1 und k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ≥ Dom(⅛)+1 und
k-Dom(⅛)+1 ∈ Dom(VERS(⅛'[^Dom(⅛')-1)) und k-Dom(⅛)+1 < i oder k-Dom(⅛)+1 =
Dom(⅛')-1
gdw
k < Dom(⅛)+1 und k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ≥ Dom(⅛)+1 und
k-Dom(⅛)+1 ∈ Dom(VERS(⅛'∣Dom(⅛')-1))∖{j' | i ≤ j < Dom(⅛')-1} oder k-Dom(⅛)+1 =
Dom(⅛')-1
gdw
k < Dom(⅛)+1 und k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ≥ Dom(⅛)+1 und k-
Dom(^)+1 ∈ Dom(VERS(⅛'))
und somit, dass Dom(VERS(⅛+)) = Dom(VERS(⅛)) и {Dom(⅛)} и {(Dom(⅛)+1+l | l ∈
Dom(VERS(⅛'))} und damit (v) gilt. Fur den Fall, dass ⅛' ∈ NEF(⅛'ΓDom(⅛')-1), zeigt
man analog, dass dann auch .A ∈ NEF(⅛*) ⊂ RGS∖{0} und v) gilt.
(PBF): Sei nun ⅛' ∈ PBF(⅛'ΓDom(⅛')-1). Dann gilt nach Definition 3-15, dass es β ∈
PAR, ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ}, und i ∈ Dom(VERS(⅛'ΓDom(⅛')-1))
gibt, so dass mit iv') rVξΔ^, = A(⅛'i) = A(^*Dom(⅛)+1+i) und [β, ξ, Δ] = A(⅛'i+1) =
A(^*Dom(^)+2+i), wobei i ∈ Dom(VANS(⅛'ΓDom(⅛')-1)) und K(⅛'ΓDom(⅛')-1) =
A(A Dom(⅛')-2) A(A Dom(⅛)+1+Dom(⅛')-2) = K(⅛*) und ⅛' = ⅛'ΓDom(⅛')-1 и {(Dom(⅛')-1,
rAlso K(⅛'ΓDom(⅛')-1)} und β ∉ TTFM({Δ, K(⅛'ΓDom(⅛')-1)}) und es gibt kein j ≤ i,
so dass β ∈ TT(⅛'j), und es gibt kein l mit i+1 < l ≤ Dom(⅛')-2, so dass l ∈
Dom(VANS(⅛TDom(⅛')-1).
Dann gilt mit iv') und v'): Dom(⅛)+1+i ∈ Dom(VERS(⅛*)) und Dom(⅛)+2+i ∈
Dom(VANS(⅛*)) und es gibt kein l mit Dom(⅛)+2+i < l ≤ Dom(⅛)+1+Dom(⅛')-2, so
dass l ∈ Dom(VANS(⅛*)). Sodann gilt mit vi'), dass .ħ' = ⅛* и
{(Dom(⅛)+1+Dom(⅛')-1, rAlso K(⅛'ΓDom(⅛')-1)} = b* и {(Dom(⅛)+1+Dom(⅛')-1,
rAlso K(⅛*)π}.
Sodann ist ξ ∈ FV(Δ) oder ξ ∉ FV(Δ). Sei nun ξ ∈ FV(Δ). Dann ist β ∈ TT([β, ξ, Δ])
⊂ TTSEQ(⅛'). Da nun nach Voraussetzung PAR ∩ TTSEQ(⅛) ∩ TTSEQ(⅛') = 0 ist
damit β ∉ TTSEQ(⅛). Damit ergibt sich mit i') bis iv') daraus, dass β ∉ TTFM({Δ,
K(⅛'ΓDom(⅛')-1)}) und es kein j ≤ i gibt, so dass β ∈ TT(⅛'j), dass auch β ∉ TTFM({Δ,