D42 Georg Meggle
(ii) G(S,K(G’(H,MI(S,H,f,r)) T(S,f))) ├
(iii) WG
1
(S,S,H’,G’(H,G(S,K(G’(H,MI(S,H,f,r)) T(S,f))))) ├
Aus KV(S,H,f,KV(S,H,f,r)) dann mit (i) bis (iii) wegen T.K80.1 schließlich
KV(S,H,f,MI(S,H,f,r)).
Für (ii) Aus T.V2 G(S,K(G’(H,T(S,f)) T(S,f))) (). Da nun
wegen D2 MI(S,H,f,r) T(S,f), wegen TG1a auch G’(H,MI(S,H,f,r))
G’(H,T(S,f)), wegen RC, C2, RG also G(S,K(G’(H,MI(S,H,f,r))
G’(H,T(S,f)))), mit () also wegen TG1c, C4, RC, C3 und TG1a
schließlich G(S,K(G’(H,MI(S,H,f,r)) T(S,f))).
Für (iii): Direkt aus (ii) durch wiederholte Anwendung von RG.
Für T.K75.8.2: KV(S,H,f,MI(S,H,f,r)) KV(S,H,f,KV(S,H,f,r))
Wir zeigen:
(i) KV(S,H,f,MI(S,H,f,r)) MI(S,H,f,KV(S,H,f,r))
und
(ii) ...