Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



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

(v)  VAN(S') VAN(S) und

(vi) Wenn VAN(S') VAN(S), dann ist S' PBF(S).

Beweis: Sei S ∈ SEQ und S' KEF(S) BEF(S) AEF(S) UEF(S) PEF(S)
IEF(S). Dann gilt mit Definition 3-18 S' RGF(S). Sodann gilt mit Definition 3-4,
Definition 3-6, Definition 3-8, Definition 3-12, Definition 3-14 und Definition 3-16: Es
gibt Α, Β
GFORM und θ GTERM und β PAR und ξ VAR und Δ FORM, wo-
bei FV(Δ)
{ξ}, so dass S' = S ∪ {(Dom(S), rAlso Α ∧ Β^l)} oder S' = S ∪
{(Dom(S), rAlso Α → Β^l)} oder S' = S ∪ {(Dom(S), rAlso Α ∨ Β^l)} oder S' = S ∪
{(Dom(S), rAlso ΛξΔ-l)} oder S' = S ∪ {(Dom(S), rAlso VξΔ-l)} oder S' = S ∪
{(Dom(S), rAlso θ = θ^l)}. Dann ist mit eindeutiger Lesbarkeit (Theorem 1-10, Theorem
1-11 und Theorem 1-12) (Dom(
S), -⅜'Dom()) ANS(S') und damit nach Definition 3-1 S'
AF(S). Dann ergeben sich (i), (ii), (iv) und (v) mit Theorem 3-17-(i), -(ii), -(iii) and
-(iv). Sodann ergibt sich mit Theorem 3-19-(x), Theorem 3-20-(x) und eindeutiger Les-
barkeit, dass
S' SEF(S) NEF(S). Damit gilt mit Theorem 3-23: Wenn VANS(S')
VANS(S), dann S' PBF(S) und somit (iii). Sei nun fur (vi): VAN(S') VAN(S).
Dann gilt VAN(
S) £ VAN(S') und damit mit Theorem 2-75 VANS(S) £ VANS(S').
Damit gilt mit (ii): VANS(
S') VANS(S) und damit mit (iii), dass S' PBF(S). ■

Theorem 3-27. VERS, VANS, VER und VAN bei SB, KB, BB, AB, NB, UB, IB

Wenn S ∈ SEQ und S' SBF(S) KBF(S) BBF(S) ABF(S) NBF(S) UBF(S)
IBF(S), dann:

(i)   VERS(S') VERS(S) {(Dom(S), ‰ms))},

(ii) VANS(S') VANS(S),

(iii) Wenn VANS(S') VANS(S), dann ist S' SEF(S) NEF(S) PBF(S),

(iv) VER(S') VER(S) {K(S')},

(v)  VAN(S') VAN(S) und

(vi) Wenn VAN(S') VAN(S), dann ist S' SEF(S) NEF(S) PBF(S).

Beweis: Sei S ∈ SEQ und S' SBF(S) KBF(S) BBF(S) ABF(S) NBF(S)
UBF(S) IBF(S). Dann gilt mit Definition 3-18 S' RGF(S). Sodann gilt mit
Definition 3-3, Definition 3-5, Definition 3-7, Definition 3-9, Definition 3-11, Definition
3-13 und Definition 3-17:
S' = S ∪ {(Dom(S), rAlso A(S'Dom(S))n)}. Dann ist (Dom(S),
S'Dom(S)) ANS(S') und damit S' AF(S). Dann ergeben sich (i), (ii), (iv) und (v) mit
Theorem 3-17-(i), -(ii), -(iii) and -(iv). Sodann ergibt sich (iii) mit Theorem 3-23. Sei nun



More intriguing information

1. Ronald Patterson, Violinist; Brooks Smith, Pianist
2. The name is absent
3. FDI Implications of Recent European Court of Justice Decision on Corporation Tax Matters
4. The name is absent
5. Kharaj and land proprietary right in the sixteenth century: An example of law and economics
6. Database Search Strategies for Proteomic Data Sets Generated by Electron Capture Dissociation Mass Spectrometry
7. Putting Globalization and Concentration in the Agri-food Sector into Context
8. Draft of paper published in:
9. The name is absent
10. The name is absent