Beweise D41
Nachtrag: Im vorgelegten Beweis für T.K75.6 wurde noch nicht von
T.K72.1 und T.K75 Gebrauch gemacht. Mit diesen ergibt sich ein Beweis
für T.K75.6 weitaus einfacher. Nämlich so: Aus I(S,f,G’(H,KV(S,H,f,r)))
nach T.K75 KV(S,H,f,KV(S,H,f,r)), und da gelten:
(i) KV(S,H,f,r) I(S,f,T’(H,r)) trivial nach T.K1
(ii) G(S,K(G’(H,I(S,f,T’(H,r))) T(S,f)))
wobei für (ii): wegen D1, TG1a, RC, C2 und RG
G(S,K(G’(H,I(S,f,T’(H,r))) G’(H,T(S,f)))), und mit
G(S,K(G’(H,T(S,f)) T(S,f))), welches aus T.V2. Womit wegen TG1c,
C4, RC, C3 und TG1e dann (ii).
Und somit durch beliebige Iteration von RG auch
(iii) WG
1
(S,S,H’,G’(H,(ii)))
Aus KV(S,H,f,KV(S,H,f,r)) also mit T.K72.1
dann KV(S,H,f,I(S,f,T’(H,r))). ...