Beweise D29
VxW(a,x=b) x(x=b W(a,x=b)) auch bereits ohne Voraussetzung
von G4 e.l. gültig – und so L.G11-1 direkt nach Metatheorem (GG
n
.1).
Für L.G12: VxGW(P,x=b) VxGW(P,x=b’) GG(P,b=b’)
Für L.G12-1: VxGW
n
(P,x=b) VxGW
n
(P,x=b’) GG
m
(P,b=b’)
für bel. m,n 1, mit m n
VxGW(P,x=b) VxGW(P,x=b’) nach L.G1 äquivalent mit Vx(x= b
GG(P,x=b)) Vx(x= b’ GG(P,x=b’)); und VxGW
n
(P,x=b)
VxGW
n
(P,x=b’) nach L.G2 äquivalent mit Vx(x= b GG
n
(P,x=b))
Vx(x= b’ GG
n
(P,x=b’)) für alle m n. Da nun aber bereits Vx(x= b
G(a,x=b)) Vx(x= b’ G(a,x=b’)) e.l. gültig ohne Voraussetzung von
G4 und G5, so L.G12 aus (GG1) und L.G12-1 aus (GG
n
.1).
L.G13: GW(P,x(GW
1
(P,xP) v GW
1
(P, (x