D64 Georg Meggle
Für (ii.1): Wir zeigen:
(ii.1.1) () WG
1
() (KV(S,H,f,r) T(S,f)
trivial nach D1, T.K1
(ii.1.2) () WG
1
() (KV(S,H,f,r)
P(S,G’(H,MI(S,H,f,r*))))
(ii.1.3) () WG
1
() (KV(S,H,f,r)
G(S,K(G’(H,MI(S,H,f,r*)),T(S,f)))))
(ii.1.4) () WG
1
() (KV(S,H,f,r)
G(S,G’(H,MI(S,H,f,r*)) T(S,f)))
Für (ii.1.2): Aus () WG
1
() und KV(S,H,f,r) mit (ii.1.3) unten
G(S,K(G’(H,MI(S,H,f,r*)),T(S,f))) und daraus mit C6, TG1e G(S,T(S,f)
G’(H,MI(S,H,f,r*))), mit P(S,T(S,f)) – letzteres aus KV(S,H,f,r) mit
T.K1 und T.I4 – somit also wegen P3 auch P(S,G’(H,MI(S,H,f,r*))).
Für (ii.1.3): Wir zeigen:
(ii.1.3.1) () WG
1
() (KV(S,H,f,r)
G(S,K(G’(H,(I(S,f,T’(H,r *)),T(S,f)))))
und
(ii.1.3.2) ...