6.1 Korrektheit des Redehandlungskalkuls 243
(KBF, AEF): Sei M ∈ KBF(MTDom(M)-1). Nach Definition 3-5 gibt es dann Δ ∈
GFORM, so dass rΔ ∧ K(M)^l ∈ VER(MTDom(M)-1) oder rK(⅛) ∧ Δ ∈
VER(MTDom(M)-1). Wegen rΔ ∧ K(M)^l ∈ VER(MTDom(M)-1) oder ∣K(M) ∧ ∆^l ∈
VER(MTDom(M)-1) gibt es j ∈ Dom(M)-1, so dass rΔ ∧ K(M)^l oder ∣K(M) ∧ ∆^l in
MTDom(M)-1 bei j verfugbar ist. Dann ist K(MTj+1) = ∣∆ ∧ K(M)^l oder K(MTj+1) =
∣K(M) ∧ ∆^l. Dann gilt VAN(MTj+1) = rΔ ∧ K(M)^l oder VAN(MTj+1) = rK(Λ) ∧ ∆^l.
Mit Theorem 3-29-(iv) gilt dann VAN(MTj+1) ⊂ VAN(MTDom(M)-1) = VAN(M) und
damit mit Theorem 5-13 auch VAN(M) = ∣∆ ∧ K(M)^l oder VAN(M) = rK(M) ∧ Δη.
Theorem 5-18 ergibt in beiden Fallen VAN(M) = K(M). Analog zeigt man fur AEF mit
Theorem 5-22, dass VAN(M) = K(M).
(ABF): Sei M ∈ ABF(MΓDom(M)-1). Nach Definition 3-9 gibt es dann Β, Δ ∈ GFORM
so dass ∣B V ∆^l, ∣B → K(M)^l, r∆ → K(M)^l ∈ VER(MΓDom(M)-1). Dann gibt es j, k, l ∈
Dom(M)-1, so dass rB v ∆^l in MΓDom(M)-1 bei j und rB → K(M)^l in MΓDom(M)-1 bei k
und ∣∆ → K(M)^l in MΓDom(M)-1 bei l verfugbar ist. Dann ist K(MTj+1) = ∣B v ∆^l und
K(MΓk+1) = ∣B → K(M)^l und K(Mtl+1) = ∣∆ → K(M)^l. Dann gilt VAN(MTj+1) = ∣B v
∆^l und VAN(MΓk+1) = ∣B → K(M)^l und VAN(MTl+1) = ∣∆ → K(M)^l. Mit Theorem
3-29-(iv) gilt sodann VAN(MΓj+1) ⊆ VAN(MΓDom(M)-1) und VAN(MΓk+1) ⊂
VAN(MΓDom(M)-1) und VAN(MTl+1) ⊆ VΛ∖(Mi□om(M)-1) und damit VAN(MTj+1) ⊆
VAN(M) und VAN(MΓk+1) ⊂ VAN(M) und VAN(MTl+1) ⊆ VAN(M). Damit gilt mit
Theorem 5-13 auch VAN(M) = ∣B v ∆^l und VAN(M) = ∣B → K(M)^l und VAN(M) =
∣∆ → K(M)^l. Theorem 5-23 ergibt VAN(M) = K(M).
(NBF, UBF, PEF): Sei M ∈ NBF(MΓDom(M)-1). Nach Definition 3-11 ist dann
r—i—ιK(M)^l ∈ VER(MΓDom(M)-1). Sodann gibt es j ∈ Dom(M)-1, so dass ∣- K(M)^l in
MTDom(M)-1 bei j verfugbar ist. Dann ist K(MTj+1) = ∣--K(M)^l. Dann gilt
VAN(MTj+1) = Г-—K(M)π. Mit Theorem 3-29-(iv) gilt sodann VAN(MTj+1) ⊆
VAN(MTDom(M)-1) = VAN(M) und daher mit Theorem 5-13 auch VAN(M) =
Г-—K(M)π. Theorem 5-26 ergibt VAN(M) = K(M). Analog zeigt man fur UBF mit
Theorem 5-28 und fur PEF mit Theorem 5-29, dass dann auch jeweils VAN(M) = K(M).
(UEF): Sei M ∈ UEF(MTDom(M)-1). Nach Definition 3-12 gibt es dann β ∈ PAR, ξ ∈
VAR und ∆ ∈ FORM, wobei FV(∆) ⊂ {ξ}, so dass [β, ξ, ∆] ∈ VER(MTDom(M)-1) und β
∉ TTFM({∆} и VAN(MTDom(M)-1)) und K(M) = ∣Λξ∆π. Dann gibt es j ∈ Dom(M)-1,
so dass [β, ξ, ∆] in MTDom(M)-1 bei j verfugbar ist. Dann ist K(MTj+1) = [β, ξ, ∆]. Dann
gilt VAN(MTj+1) = [β, ξ, ∆]. Mit Theorem 3-29-(iv) gilt sodann VAN(MTj+1) ⊆