D82 Georg Meggle
(iv.2) () G(S,G’(H,()))
(MI(S,H,f,r) G(S,K(G’(H,I(S,f,T’(H,r))) T(S,f))))
und daraus dann mit TG1c, C4, RC, C3, TG1e (iv).
Für (iv.1): Wir zeigen
(iv.1.1) () G(S,G’(H,())) (MI(S,H,f,r)
G(S,K(T’(H,r) T(S,f))))
Und daraus dann mit () wegen TG1c, C4, RC, C3, TG1e (iv.1).
Für (iv.1.1): Aus MI(S,H,f,r) nach D2 G(S,K(T’(H,r)
G’(H,I(S,f,T’(H,r))))) und daraus nach RC, C3, TG1e (1) G(S,K(T’(H,r)
G’(H,I(S,f,T’(H,r))))). Da nun aber wegen D1 I(S,f,T’(H,r)) T(S,f) ├,
wegen TG1a auch G’(H,I(S,f,T’(H,r)) G’(H,T(S,f))), mit RC, C2 und
RG auch (2) G(S,K(G’(H,I(S,f,T’(H,r))) G’(H,T(S,f)))). Nun aber we-
gen T.V.2 und RC, C3, TG1e auch G(S,K(G’(H,T(S,f)) T(S,f))), mit (2) ...