Voraussetzungen und Prinzipien C9
T.K9: KV(S,H,f,r) G(S,G´(H,I))
G(S,K(G´(H,I),T(S,f))) G(S,G´(H,I) T(S,f))
T.K10: KV(S,H,f,r) G(S,T´(H,r))
G(S,K(T´(H,r),T(S,f))) G(S,T`(H,r) T(S,f))
T.K11: KV(S,H,f,r) G(S,G’(H,I)) G(S,K(G´(H,I)))
G(S,K(G´(H,I),I)) G(S,G´(H,I) I)
T.K12: KV(S,H,f,r) G(S,G’(H,I))
G(S,K(G´(H,I),G’(H,T(S,f)))) G(S,G´(H,I)
G´(H,T(S,f)))
T.K13: KV(S,H,f,r) G(S,T‘(H,r))
G(S,K(T´(H,r),G’(H,T(S,f)))) G(S,T´(H,r)
G´(H,T(S,f)))
T.K14: KV(S,H,f,r) G(S,T´(H,r))
G(S,K(T´(H,r),G´(H,I))) G(S,T´(H,r) G´(H,I))
T.K15: VKV
i
(Y,S,H,f) KV
i
(S,H,f)
p(KV(S,H,f,p) W(Y,KV(S,H,f,p)))
T.K16: VKV(Y,S,H,f) KV(S,H,f)