Beweise D9
Die verwendeten Abkürzungen:
(0.)* xGW(P,B(x)) v GW(P,B(x)))
(0.)
n
* xGW
n
(P,B(x)) v GW
n
(P,B(x)))
wobei
L.G9: (0.)* (0..1)* (0..2)*
L.G9-1: (0.)
n
* (0. .1)
n
* (0..2)
n
mit
(0.1)* x(B(x) GG(P,B(x)))
(0..1)
n
* x(B(x) GG
n
(P,B(x)))
und
(0..2)* x(B(x) GG(P,B(x)))
(0..2)
n
* x(B(x) GG
n
(P,B(x)))
Ferner:
(0.) x(x=b
1
v … v x=b
m
B(x))
(0.) also äquivalent mit der Konjunktion von
(0..1) x(x=b
1
v … v x=b
m
B(x))
und
(0..2) x(B(x) x=b
1
v … v x=b
m
))
und
(QV*
B
)* VxGW(P,x=b
1
) … VxGW(P,x=b
m
)
(QV*
B
)
n
* VxGW
n
(P,x=b
1
) … VxGW
n
(P,x=b
m
)