Voraussetzungen und Prinzipien C21
T.K79: G(S,K(T’(H,r) T’(H,r*)))
WG
1
(S,S,H,G’(H,G(S,K(T’(H,r) T’(H,r*)))))
(KV(S,H,f,r) KV(S,H,f,r*))
T.K79.1: G(S,K(G’(H,A) G’(H,B)))
WG
1
(S,S,H,G’(H,G(S,K(G’(H,A) G’(H,B)))))
(KV(S,H,f,A) KV(S,H,f,B))
T.K79.2: G(S,K(G’(H,p) G’(H,G(S,p))))
WG
1
(S,S,H,G’(H,G(S,K(G’(H,p) G’(H,G(S,p))))))
(KV(S,H,f,p) KV(S,H,f,G(S,p)))
T.K80: T’(H,r) T’(H,r*) ├
KV(S,H,f,r) (G(S,K(T’(H,r*) T(S,f)))
WG
1
(S,S,H’,G’(H,G
0
(S,T’H,r*) T(S,f)))))
KV(S,H,f,r*))
Für T.K80.1: A B ├
KV(S,H,f,A) (G(S,K(G’(H,B)) T(S,f)))
WG
1
(S,S,H’,G’(H,G
0
(S,K(G’(H,B) T(S,f)))))
KV(S,H,f,B))
T.K81: KV(S,H,f,r) I(S,f,G’(H,KV(S,H,f,r))) I(S,f,T’(H,r))
G(S,