D60 Georg Meggle
und
(ii.3.2): IE(S,f,G’(H,KV(S,H,f,r)))
K(G’(H,KV(S,H,f,MI(S,H,f,r))) T(S,f))
Und daraus dann mit C4, RC und C3 (ii.3).
Für (ii.3.1): Wir zeigen:
(ii.3.1.1) IE(S,f,G’(H,KV(S,H,f,r)))
K(G’(H,MI(S,H,f,r)) T(S,f))
und
(ii.3.1.2) IE(S,f,G’(H,KV(S,H,f,r)))
K(T(S,f) G’(H,MI(S,H,f,r)))
Und daraus dann wegen C4, RC, C3 (ii.3.1)
Für (ii.3.1.1): Aus V5.E K(G’(H,T(S,f)),T(S,f)). Da aus
G’(H,T(S,f)) nach G1 G’(H,T(S,f)), mit RC, C3 also
K(G’(H,T(S,f)),T(S,f)). Mit K(T(S,f)) – aus T.V1.E – mit C5 also
K(T(S,f) G’(H,T(S,f))), mit RC, C3 also K(G’(H,T(S,f)) T(S,f))
(). Nun aber wegen D2 MI(S,H,f,r) T(S,f), mit TG1a also
G’(H,MI(S,H,f,r)) G’(H,T(S,f)), ...