D70 Georg Meggle
(ii.1.4) T’(H,r) T’(H,r*) ├ KV(S,H,f,r) (() ()
G(S,G’(H,MI(S,H,f,r*)) T(S,f))))
Für (ii.1.1): Trivial nach T.K1 und D1.
Für (ii.1.2): Aus den gegebenen Prämissen nach (ii.1.3)
G(S,K(G’(H,MI(S,H,f,r*)),T(S,f))), nach C6, RG, TG1c, TG1e also (1)
G(S,T(S,f) G’(H,MI(S,H,f,r*))); da (2) P(S,T(S,f)) – aus KV(S,H,f,r)
zunächst nach T.K1 I(S,f,T’(H,r)) und daraus nach T.I4 dann (2) – aus (1)
und (2) mit P5 also auch P((SS,G’(H,MI(S,H,f,r*))).
Für (ii.1.3): Aus KV(S,H,f,r) nach T.K22 I(S,f,G’(H,KV(S,H,f,r)))
und daraus dann nach D1 (1) G(S,K(G’(H,KV(S,H,f,r)),T(S,f))). Da aus
KV(S,H,f,r) nach T.K0 MI(S,H,f,r), mit RG also auch G’(H,KV(S,H,f,r)
MI(S,H,f,r)), mit RC und