D20 Georg Meggle
Aus VxGW
n
(P,x=b) nach L.G2 VxGG
n
(P,x=b) und somit wegen T.G11-
1a auch T.G11-1.
T.G11-1a: VxGG
n
(P,x=b) (GG
n
(P,F(b)) Vx(x=b
GG
n
(P,F(x)))) für beliebige n 1
Das entsprechende G-Prinzip gilt bereits ohne G4 und G5 – und so
T.G11-1a direkt nach Metatheorem (GG
n
.1).
Für
T.G12: GG(P,b=b’) (GG(P,F(b)) GG(P,F(b’)))
T.G12-1: GG
n
(P,b=b’) (GG
n
(P,F(b)) GG
n
(P,F(b’))) für bel. n 1
Die entsprechenden G-Prinzipien gelten e.l. bereits ohne Voraussetzung
von G4 und G5 – und somit T.G12 und T.G12-1 direkt nach (GG.1) bzw.
(GG
n
.1).
Für T.G13: x(GW(P,B(x)) v GW(P, B(x)))
(GG(P,x(B(x) F(x))) x(B(x) GG(P,F(x))))
x(GW(P,B(x)) v GW(P, B(x))) nach L.G9 äquivalent mit (a) x(B(x)
GG( ...