Beweise D73
Für T.K81.1: Aus KV(S,H,f,r) nach T.K22 I(S,f,G’(H,KV(S,H,f,r)))
und nach T.K1 I(S,f,T’(H,r)); G(S,K(T’(H,r) T(S,f))) aus KV(S,H,f,r)
schließlich so: Zunächst nach T.K0 MI(S,H,f,r) und daraus nach D2 ()
G(S,K(T’(H,r) G’(H,I(S,f,T’(H,r))))). Da nach D1 I(S,f,T’(H,r)) T(S,f)
├ , nach RG und G1 G’(H,I(S,f,T’(H,r))) G’(H,T(S,f)) ├, mit RC und
C2 also K(G’(H,I(S,f,T’(H,r))) G’(H,T(S,f))) ├, mit RG also
G(S,K(G’(H,I(S,f,T’(H,r))) G’(H,T(S,f)))), mit G(S,K(T’(H,r)
G’(H,I(S,f,T’(H,r))))) – aus () mit RC, C3, RG und TG1e – also wegen
C4, RC, C3, G, TG1e und TG1c dann G(S,K(T’(H,r) G’(H,T(S,f)))),
mit G(S,K(G’(H, T(S,f)) T(S,f))) – aus T.V2 mit RC, C4, RG und
TG1e – ebenso dann ...