2.3 VERS, VANS, VER und VAN 105
Definition 2-30. Zuordnung der Menge der verfugbaren Aussagen (VER)
VER = {(ft, X) | ft ∈ SEQ und X = {Γ | Es gibt ein i ∈ Dom(VERS(ft)) und Γ = A(fti)}}.
Definition 2-31. Zuordnung der Menge der verfugbaren Annahmen (VAN)
VAN = {(ft, X) | ft ∈ SEQ und X = {Γ∣ Es gibt ein i ∈ Dom(VANS(ft)) und Γ = A(fti)}}.
Theorem 2-71. Verhaltnis von VAN und VER
Wenn ft ∈ SEQ, dann VAN(ft) ⊆ VER(ft).
Beweis: Ergibt sich mit Theorem 2-70 direkt aus den Definitionen. ■
Theorem 2-72. VERS-Inklusion impliziert VANS-Inklusion
Wenn ft, ft' ∈ SEQ und VERS(ft) ⊆ VERS(ft'), dann VANS(ft) ⊆ VANS(ft').
Beweis: Seien ft, ft' ∈ SEQ und sei VERS(ft) ⊆ VERS(ft'). Sei nun (i, fti) ∈ VANS(ft).
Dann ist (i, fti) ∈ VERS(ft) ∩ ANS(ft). Dann ist (i, fti) ∈ VERS(ft) und fti ∈ ASATZ.
Dann ist nach Voraussetzung (i, fti) ∈ VERS(ft') und somit auch (i, fti) ∈ ft'. Da fti ∈
ASATZ, ist damit (i, fti) ∈ ANS(ft') und damit insgesamt (i, fti) ∈ VERS(ft') ∩ ANS(ft')
= VANS(ft'). ■
Theorem 2-73. VANS-Verringerung impliziert VERS-Verringerung
Wenn ft, ft' ∈ SEQ und VANS(ft)∖VANS(ft') ≠ 0, dann VERS(ft)∖VERS(ft') ≠ 0.
Beweis: Seien ft, ft' ∈ SEQ und sei VANS(ft)∖VANS(ft') ≠ 0. Dann ist VANS(ft) £
VANS(ft') und mit Theorem 2-72 folgt VERS(ft) £ VERS(ft') und daher
VERS(ft)∖VERS(ft') ≠ 0. ■
Theorem 2-74. VERS-Inklusion impliziert VER-Inklusion
Wenn ft, ft' ∈ SEQ und VERS(ft) ⊆ VERS(ft'), dann VER(ft) ⊆ VER(ft').
Beweis: Seien ft, ft' ∈ SEQ und sei VERS(ft) ⊆ VERS(ft'). Sei nun Γ ∈ VER(ft). Dann
gibt es ein i ∈ Dom(VERS(ft)), so dass Γ = A(fti). Dann ist (i, fti) ∈ VERS(ft). Nach Vo-
raussetzung ist dann (i, fti) ∈ VERS(ft'). Nun ist VERS(ft') ⊆ ft' und somit (i, fti) ∈ ft'
und also fti = ft'i. Somit ist Γ = A(fti) = A(ft'i). Also ist insgesamt i ∈ Dom(VERS(ft'))
und Γ = A(ft'i). Also ist Γ ∈ VER(ft'). ■