Beweise D77
Mit T’(H,r) T’(H,r*) ├ dann aus (1) und (2) wegen TG1c, RC, C4, RG,
TG1e und T.I10 also G(S,K(G’(H,I(S,f,T’(H,r*))),T(S,f))), mit
G(SKT(S,f)) – d.h. TV.1 – wegen TG1e, C5, RG, TG1e also
G(S,K(T(S,f) G’(H,I(S,f,T’(H,r*))))).
Für L.20.1: A B ├ MI (S,H,f,A) (G(S,K(G’(H,B)) T(S,f)))
G(S,G’(H,G(S,K(G’(H,B) T(S,f))))) MI(S,H,f,B))
Es gilt bereits, wie sich bei Einsetzung von G’(H,p) für T’(H,r) und von
G’(H,B) für T’(H,r*) aus dem Beweis für L.20 ergibt, das Lemma
(i) G’(H,A) G’(H,B) ├ MI(S,H,f,A) (G(S,K(G’(H,B))
T(S,f))) G(S,G’(H,G(S,K(G’(H,B) T(S,f))))) MI(S,H,f,B))
und somit dann, da wegen TG1a A B ├ G’(H,A) G’(H,B) gilt, erst
recht L.20.1.
Für L.21: G(S,G’(H,G ...