C16 Georg Meggle
T.G7: GG(P,A B) (GG(P,A) GG(P,B))
T.G7-1: GG
n
(P,A B) (GG
n
(P,A) GG
n
(P,B)) für bel. n 1
T.G7*: GW(P,A B) (GW(P,A) GW(P,B))
T.G7*-1: GW
n
(P,A B) (GW
n
(P,A) GW
n
(P,B)) für bel. n 1
Des Weiteren gelten:
T.G8: GG(P,A) GW(P,GG(P,A))
T.G9: GG(P,A) GG(P,GW(P,A))
T.G10: GW(P,A) GG(P,GW(P,A))
T.G11: VxGW(P,x=b) (GG(P,F(b)) Vx(x=b GG(P,F(x))))
T.G11-1: VxGW
n
(P,x=b) (GG
m
(P,F(b)) Vx(x=b GG
m
(P,F(x))))
für beliebige m,n 1, mit m n
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 beliebige n 1
T.G13: x(GW(P,B(x)) ˅ GW(P, B(x)))
(GG(P,x(B(x) F(x))) x(B(x) GG(P,F(x))))
T.G13-1: x(GW
n
(P,B(x))