Beweise D45
G(S,K(G’(H,KV(S,H,f,r)) G’(H,T(S,f)))), mit G(S,K(G’(H,T(S,f))
T(S,f)) also wegen TC1c, C4, RC, C3 und TG1e schließlich
G(S,K(G’(H,KV(S,H,f,r)) T(S,f)))
Für (i.4.1.2): Wir zeigen:
(i.4.1.2.1) KV(S,H,f,MI(S,H,f,r))
G(S,K(T(S,f) G’(H,MI(S,H,f,r))))
und
(i.4.1.2.2) KV(S,H,f,MI(S,H,f,r))
G(S,K(T(S,f) G’(H,I*(S,H,f,MI(S,H,f,r)))))
Und damit dann wegen TG1c, C4, RC und C3:
(i.4.1.3) KV(S,H,f,MI(S,H,f,r))
G(S,K(T(S,f) G’(H,MI(S,H,f,r)
I*(S,H,f,MI(S,H,f,r)))))
Und somit wegen T.K42, RG, TG1c, RC, C3 schließlich (i.4.1.2).
Für (i.4.1.2.1): Aus KV(S,H,f,MI(S,H,f,r)) nach T.K1
I(S,f,G’(H,MI(S,H,f,r))) und daraus nach D1
G(S,K(G’(H,MI(S,H,f,r)),T(S,f))), mit G(S, ...