D50 Georg Meggle
G(S,K(G’(H,G(S,K(G’(H,G(S,K(T(S,f) G’(H,I)))),T(S,f)))),T(S,f))).
Und da G(S,K(G’(H,T(S,f)),T(S,f))) – aus V5 – wegen TG1c, C4, RC, C3
und TG1e also wegen V2.1 auch G(S,K(G’(H,G(S,G’(H,G(S,K(T(S,f)
G’(H,I)))))),T(S,f))).
Für (i.4): WG
1
(KV(S,H,f,I) G(S,K(G’(H,MI)
G’(H,I(S,f,G’(H,MI))))))
Wir zeigen:
(i.4.1) WG
1
(KV(S,H,f,I) G(S,K(G’(H,MI) T(S,f))))
und
(i.4.2) WG
1
(KV(S,H,f,I) G(S,K(G’(H,I(S,f,G’(H,MI)))
T(S,f))))
Und daraus dann mit TG1c, C4, RC, C3 und TG1e (i.4).
Für (i.4.1): Wir zeigen:
(i.4.1.1) WG
1
(KV(S,H,f,I) G(S,K(G’(H,MI) T(S,f))))
und
(i.4.1.2) WG
1
(KV(S,H,f,I) G(S,K(T(S,f) G’(H,MI))))
Und daraus dann mit TG1c, C4, RC, C3 und TG1e (i.4.1). ...