Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.3 VERS, VANS, VER und VAN in Ableitungen und bei einzelnen Ubergangen 145

2-83-(iv) bis -(xi) und mit der eindeutigen Bestimmtheit geschlossener Abschnitte mit
demselben Endglied (Theorem 2-53) die restlichen Klauseln ((ii) bis (ix)). ■

Theorem 3-20. VERS, VANS, VER und VAN bei NE

Wenn S ∈ SEQ und S' ∈ NEF(S), dann:

(i)   {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)} ist ein NE-geschlossener Abschnitt in

S',

(ii) VERS(S)∖VERS(S') ⊂ {(j, Sj) | ma∖(Dom(VANS(⅛))) ≤ j < Dom(S)},

(iii) VERS(S') = (VERS(S)∖{(j, Sj) | max(Dom(VANS(S))) ≤ j < Dom(S)}) ∪
{(Dom(S), S'Dom(S))},

(iv) VANS(S)∖VANS(S') = {(max(Dom(VANS(S))), s'.    ..     . )},

(v)   VANS(.) = VANS(S') и {(max(Dom(VANS(S))), S'max(Dom(VANS(s))))},

(vi) VER(S)∖VER(S') ⊂ {A(S j) | max(Dom(VANS(S))) ≤ j < Dom(S)},

(vii) VER(S) ⊂ {A(S'j) | j ∈ Dom(VERS(S')iDom(S))} и

{A(S j) | max(Dom(VANS(S))) ≤ j < Dom(S)},

(viii) VAN(S)∖VAN(S') ⊂ {A(S'max(Dom(VANS(S))))},

(ix) VAN(S) = VAN(S') и {A(S'max(Dom(VANS(S))))} und
(x)    K(S') =    A(Smax(Dom(VANS(S)))) ∙

Beweis: Sei S ∈ SEQ und S' ∈ NEF(S)∙ Dann gilt mit Definition 3-18 S' ∈ RGF(S)∙
Sodann gilt mit Definition 3-10: Es gibt Δ, Γ ∈ GFORM und i, j ∈ Dom(S), so dass i ≤ j,
A(Si) = Δ und (i, Si) ∈ VANS(S), A(Sj) = Γ und A(Sdo.(s)-i) = ` ɪ oder A(Sj) =
^r—Γ^^l und A(SDom(S)-I) = Γ und (j, Sj) ∈ VERS(S) und es gibt kein l mit i < l ≤
Dom(S)-I, so dass (l, S_l) ∈ VANS(S), und S' = S и {(Dom(S), ^rAlso — Δ^^l)} und somit
S' ∈ SEQ und S'ΓDom(S')-1 = STDom(S) = S∙

Sodann ist ® = {(j, S'j) | i ≤ j ≤ Dom(S)} ein Abschnitt in S' und A(S'_i) = Δ und (i, S'_i)
∈ VANS(S'ΓDom(S)) und A(S'j) = Γ und A(S'_Dom(s>i) = r—Γ oder A(S'j) = r—Γ und
A(S'D_om(s)-ι) = Γ und (j, S'j) ∈ VERS(STDom(S)) und es gibt kein l mit i < l ≤
Dom(S)-I, so dass (l, S'_l) ∈ VANS(S'ΓDom(S)) und A(S'_Dom(_S)) = r—Δ^^l. Damit gilt mit
Theorem 2-92, dass ® ein NE-geschlossener und damit auch ein geschlossener Abschnitt
in S' ist.

Da sodann max(Dom(Φ)) = Dom(S) = Dom(S')-1, ergibt sich mit Theorem 2-86,
dass   VANS(S'ΓDom(S')-1)∖VANS(S')    =    {(min(Dom(Φ)), ^S min(Dom(Φ)))}

{(max(Dom(VANS(S'ΓDom(S')-1))), ^S max(Dom(VANS(S'fDom(S')-1))))}∙ ^{Da S S} T^{Dom(S )-1}
folgt    daraus: VANS(S)∖VANS(S')    =    {(min(Dom(S)), ^S min(Dom(Φ)))}

{(max(Dom(VANS(S))), S'max(Dom(VANS(s))))} ∙ Damit ist i = min(Dom(Φ)) =

<<   119   120   121   122   123   124   125   >>

More intriguing information