D76 Georg Meggle
Für (iii): Aus MI(S,H,f,r) nach D2 (1)
G(S,K(G’(H,I(S,f,T’(H,r))),T(S,f))). Aus (1) und () mit T’(H,r)
T’(H,r*) ├ , genau wie in Beweis für (i.3) für T.K73
G(S,K(G’(H,I(S,f,T’(H,r*))),T(S,f))).
Für (iv): Wir zeigen:
(iv.1) T’(H,r) T’(H,r*) ├ MI(S,H,f,r) (() ()
G(S,K(T’(H,r*) T(S,f))))
(iv.2) T’(H,r) T’(H,r*) ├ 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 und C2 (iv).
Für (iv.1): Aus MI(S,H,f,r) nach D2 G(S,K(T’(H,r),T(S,f))) und daraus
dann – genau wie in (i.4.1) von Beweis T.K73 – mit G(S,K(T’(H,r*)
T(S,f))) und T’(H,r) T’(H,r*) ├ dann G(S,K(T’(H,r*) T(S,f))).
Für (iv.2): T’(H,r) T’(H,r*) ├ MI(S,H,f,r) ...