Beweise D47
I(S,f,G’(H,I(S,f,G’(H,I*(S,H,f,MI(S,H,f,r)))))). Mit D1 daraus
G(S,K(G’(H,I(S,f,G’(H,I*(S,H,f,MI(S,H,f,r))))),T(S,f))), und mit T.V1
wegen TG1c, C5 und TG1e schließlich G(S,K(T(S,f)
G’(H,I(S,f,G’(H,I*(S,H,f,MI(S,H,f,r)))))
Für (ii): KV(S,H,f,MI(S,H,f,r)) I*(S,H,f,MI(S,H,f,KV(S,H,f,r)))
Aus KV(S,H,f,MI(S,H,f,r)) nach T.K67.1a – mit G’(H,p) für T’(H,r) und
MI(S,H,f,r) für p – KV(S,H,f,KV(S,H,f,MI(S,H,f,r))). Daraus mit dem
eben bewiesenen Satz
(i) KV(S,H,f,MI(S,H,f,r)) MI(S,H,f,KV(S,H,f,r))
und den gleich noch zu beweisenden Sätzen
() G(S,K(G’(H,MI(S,H,f,KV(S,H,f,r))) T(S,f)))
() WG
1
(S,S,H’,G’(H,()))
mit Hilfe von T.K72.1 direkt KV(S,H,f,MI(S,H,f,KV(S,H,f,r))). Und da-
raus mit ...