D44 Georg Meggle
() G(S,K(G’(H,G(S,G’(H,KV(S,H,f,r)) T(S,f))),T(S,f)))
aus (i.3.3) und () mit TG1c, C4, T.I0, RC, C2, C3 dann also mit T.K42.1
(i.3).
Für (i.3.1): Aus KV(S,H,f,MI(S,H,f,r)) nach T.35 I*(S,H,f,MI(S,H,f,r)),
d.h. nach D9 insbesondere I
2
(S,H,f,MI(S,H,f,r)), nach D9
also I
1
(S,H,f,I
1
(S,H,f,MI(S,H,f,r))), nach D9 also
I(S,f,G’(H,I(S,f,G’(H,MI(S,H,f,r)))), nach D1 also
G(S,K(G’(H,I(S,f,G’(H,MI(S,H,f,r)))),T(S,f))).
Für (i.3.2): Aus KV(S,H,f,MI(S,H,f,r)) nach T.37
I*(S,H,f,I*(S,H,f,MI(S,H,f,r))), d.h. nach D9 insbesondere
I
2
(S,H,f,I*(S,H,f,MI(S,H,f,r))), nach D9 also
I(S,f,G’(H,I(S,f,G’(H,I*(S,H,f,MI(S,H,f,r)))))), mit D1 also
G(S,K(G’(H,I(S,f,G’(H,I*(S,H,f,MI(S,H,f,r))))),T(S,f))).
Für (i.4): ...