D84 Georg Meggle
Und
T.C3.2: WG(P(s),T(Ŷ,f) KR(Ŷ,P(s),f)) X(XP(s)
G(X,T(X,f)) KR(X,P(s),f)))
GG(P(s), X(XP(s) T(X,f)) KR(P(s),f)))
Für T.C3.1 zeigen wir:
(i) GG(P(s),X(XP(s) T(X,f)) KR(P(s),f)))
(a) WG(P(s),T(Ŷ,f))
(ii) GG(P(s),X(XP(s) T(X,f)) KR(P(s),f)))
(b) WG(P(s),KR(Ŷ,P(s),f))
(iii) GG(P(s),X(XP(s) T(X,f)) KR(P(s),f)))
(c) X(XP(s) G(X,T(X,f))
(iv) GG(P(s),X(XP(s) T(X,f)) KR(P(s),f)))
(d) X(XP(s) KR(X,P(s),f)))
Und aus (i) bis (iv) dann mit T.G21 und bereits p.l. dann T.C3.1.
Für (i): Bereits aus GG(P(s),X(XP(s) T(X,f)) alleine – und dies
aus GG(P(s),X(XP(s) T(X,f)) KR(P(s),f))) direkt nach T.G6.1 –
mit T.G26 (a).
Für (ii): Aus GG( ...