D32 Georg Meggle
T.K74: RVAKV(Y,S,H,f,r) W(Y,VAKV(S,S,H,f,r))
Dazu zu zeigen:
T.K74.a: RVAKV(Y,S,H,f,r) W(Y,VAKV(S,S,H,f,r))
und
T.K74.b: W(Y,VAKV(S,S,H,f,r)) RVAKV(Y,S,H,f,r)
Für T.K74.a: Aus RVAKV(Y,S,H,f,r) nach D4.2 VAKV(Y,S,H,f,r)
und KV(S,H,f,r). Aus letzterem einerseits mit T.K1 und D1 sowohl T(S,f),
mit P0 also auch f(S) (α), andererseits mit T.K44 auch G(S,KV(S,H,f,r))
(), woraus mit G4 dann direkt G(S,G(S,KV(S,H,f,r))).. Zusammen wegen
TG1d also auch G(S,f(S) G(S,KV(S,H,f,r))), mit D3.2 also auch
G(S,VAKV(S,S,H,f,r)). Mit diesem dann nach D0 wegen (α) und () –
zusammen nach D3.2 VAKV(S,S,H,f,r)) – schließlich
W(Y,VAKV(S,S,H,f,r)).
Für T.K74.b: Aus W(Y,VAKV(S,S,H,f,r)) zum ...