Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.3 VERS, VANS, VER und VAN 107

Injektion von VAN(W) in VANS(W)∖{(j, Wj)}) und somit k = ∣VAN(W)∣ ≤ k-1. Wider-
spruch! ■

Theorem 2-79. VERS, VANS, VER und VAN in Verkettungen mit ein-gliedrigen Sequenzen
Wenn W, W' ∈ SEQ und Dom(W') = 1, dann:

(i)   VERS(WWf) ⊆ VERS(W) и {(Dom(W), W'o)},

(ii)   VANS(W~W') ⊆ VANS(W) и {(Dom(W), W'o)},

(iii) VER(WW) ⊆ VER(W) и {K(W')},

(iv) VAN(WW) ⊆ VAN(W) и {K(W')}.

Beweis: Seien W, W ∈ SEQ und sei Dom(W') = 1.

Zu (i): Sei (i, (WW)_i) ∈ VERS(WW). Dann ist i ∈ Dom(WW) und A((WW)_i) ist in
WW bei i verfugbar. Sodann ist i ∈ Dom(W) oder i = Dom(W).

Sei nun i ∈ Dom(W). Dann ist (WW)_i = W_i. Ware nun A(W) = A((WW)_i) in W bei i
nicht verfugbar. Dann gabe es nach Definition 2-26 ein W so dass V ein geschlossener
Abschnitt in W ist und min(Dom(^)) ≤ i < max(Dom(W)). Mit Theorem 2-62-(viii) ware
dann wegen W ⊆ WW allerdings V auch ein geschlossener Abschnitt in WW' und
min(Dom(W)) ≤ i < max(Dom(^)). Damit ware A((WW)_i) aber in WW' bei i nicht ver-
fugbar. Also ist i ∈ Dom(W) und A((WW)_i) ist in W bei i verfugbar und somit (i, (WW)_i)
∈ VERS(W).

Sei nun i = Dom(W). Dann ist (WW)_i = (WW‰m(⅛) = W'o und damit (i, (WW)_i) =
(Dom(W), W'o) ∈ {(Dom(W), W'o)}.

Zu (ii): Sei (i, (WW)i) ∈ VANS(W^W'). Dann ist mit Theorem 2-70 (i, (W^W')j) ∈
VERS(WW) und (WW)i ∈ ASATZ. Dann ist mit (i) (i, (WW)i) ∈ VERS(W) ∪
{(Dom(W), W'o)}. Angenommen (i, (WW')i) ∉ {(Dom(W), W'o)}. Dann ist (i, (WW)_i) ∈
VERS(W). Dann ist (i, (WW)_i) ∈ VERS(W) und (WW)_i ∈ ASATZ und damit ist (i,
(WW)i) ∈ VANS(W).

Zu (iii): Sei Γ ∈ VER(WWf). Dann gibt es ein i ∈ Dom(WWf), so dass Γ in WWf bei i
verfugbar ist. Dann ist Γ = A((WW)_i) und (i, (WW')_i) ∈ VERS(WWf). Damit ist mit (i)
(i, (WW)_i) ∈ VERS(W) и {(Dom(W), W'_o)}. Sei nun (i, (WW')_i) ∈ VERS(W). Dann ist i
∈ Dom(VERS(W)) und W_i = (WW)_i und somit Γ = A(W_i) ∈ VER(W). Sei nun (i, (WW ')_i)
∈ {(Dom(W), W'_o)}. Dann ist i = Dom(W) und (WW)_i = W'_o und somit Γ = A(W'_o) = K(W')
∈ {K(W')}.

<<   82   83   84   85   86   87   88   >>

More intriguing information