D80 Georg Meggle
Und daraus dann nach D2’
(v) () G(S,G’(H,())) (MI(S,H,f,r) MI(S,T’(H,r*)))
Und somit, mit Vertauschung von r und r*, direkt L.22.
Für (ii): Aus (), G(S,G’(H,())) und MI(S,H,f,r) nach (iv.1) unten
G(S,K(T’(H,r*) T(S,f))) und daraus mit RC, C3 und TG1e
G(S,K(T(S,f) T’(H,r*))), mit TC12c und TG1c, TG1e also wegen
G(S,KT(S,f)), d.h. T.V1, aus G(S,K(T’(H,r*),T(S,f))) und mit C6,
TG1e somit G(S,T(S,f) T’(H,r*)) und daraus dann mit P(S,T(S,f)) –
aus MI(S,H,f,r) wegen L.1, TI4 – wegen P3 auch P(S,T’(H,r*)).
Für (iii): () G(S,G’(H,())) (MI(S,H,f,r)
G(S,K(G’(H,I(S,f,T’(H,r*))),T(S,f))))
Wir zeigen:
(iii.1) () G(S,G’(H,())) (MI(S,H,f,r)
G(S,K(G’(H,T(S,f)),T(S,f)))) ...