begin
theorem
for
g0,
g1,
g2,
g3,
g4,
g5,
g6,
g7,
g8,
g9,
g10,
g11,
g12,
a0,
a1,
a2,
a3,
a4,
a5,
a6,
a7,
a8,
a9,
a10,
a11,
b0,
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
p being
set holds
not ( not
g12 is
empty & ( not
b0 is
empty implies not
XOR2 p,
(AND2 g0,a11) is
empty ) & ( not
XOR2 p,
(AND2 g0,a11) is
empty implies not
b0 is
empty ) & ( not
b1 is
empty implies not
XOR2 a0,
(AND2 g1,a11) is
empty ) & ( not
XOR2 a0,
(AND2 g1,a11) is
empty implies not
b1 is
empty ) & ( not
b2 is
empty implies not
XOR2 a1,
(AND2 g2,a11) is
empty ) & ( not
XOR2 a1,
(AND2 g2,a11) is
empty implies not
b2 is
empty ) & ( not
b3 is
empty implies not
XOR2 a2,
(AND2 g3,a11) is
empty ) & ( not
XOR2 a2,
(AND2 g3,a11) is
empty implies not
b3 is
empty ) & ( not
b4 is
empty implies not
XOR2 a3,
(AND2 g4,a11) is
empty ) & ( not
XOR2 a3,
(AND2 g4,a11) is
empty implies not
b4 is
empty ) & ( not
b5 is
empty implies not
XOR2 a4,
(AND2 g5,a11) is
empty ) & ( not
XOR2 a4,
(AND2 g5,a11) is
empty implies not
b5 is
empty ) & ( not
b6 is
empty implies not
XOR2 a5,
(AND2 g6,a11) is
empty ) & ( not
XOR2 a5,
(AND2 g6,a11) is
empty implies not
b6 is
empty ) & ( not
b7 is
empty implies not
XOR2 a6,
(AND2 g7,a11) is
empty ) & ( not
XOR2 a6,
(AND2 g7,a11) is
empty implies not
b7 is
empty ) & ( not
b8 is
empty implies not
XOR2 a7,
(AND2 g8,a11) is
empty ) & ( not
XOR2 a7,
(AND2 g8,a11) is
empty implies not
b8 is
empty ) & ( not
b9 is
empty implies not
XOR2 a8,
(AND2 g9,a11) is
empty ) & ( not
XOR2 a8,
(AND2 g9,a11) is
empty implies not
b9 is
empty ) & ( not
b10 is
empty implies not
XOR2 a9,
(AND2 g10,a11) is
empty ) & ( not
XOR2 a9,
(AND2 g10,a11) is
empty implies not
b10 is
empty ) & ( not
b11 is
empty implies not
XOR2 a10,
(AND2 g11,a11) is
empty ) & ( not
XOR2 a10,
(AND2 g11,a11) is
empty implies not
b11 is
empty ) & not ( ( not
a11 is
empty implies not
AND2 g12,
a11 is
empty ) & ( not
AND2 g12,
a11 is
empty implies not
a11 is
empty ) & ( not
a10 is
empty implies not
XOR2 b11,
(AND2 g11,a11) is
empty ) & ( not
XOR2 b11,
(AND2 g11,a11) is
empty implies not
a10 is
empty ) & ( not
a9 is
empty implies not
XOR2 b10,
(AND2 g10,a11) is
empty ) & ( not
XOR2 b10,
(AND2 g10,a11) is
empty implies not
a9 is
empty ) & ( not
a8 is
empty implies not
XOR2 b9,
(AND2 g9,a11) is
empty ) & ( not
XOR2 b9,
(AND2 g9,a11) is
empty implies not
a8 is
empty ) & ( not
a7 is
empty implies not
XOR2 b8,
(AND2 g8,a11) is
empty ) & ( not
XOR2 b8,
(AND2 g8,a11) is
empty implies not
a7 is
empty ) & ( not
a6 is
empty implies not
XOR2 b7,
(AND2 g7,a11) is
empty ) & ( not
XOR2 b7,
(AND2 g7,a11) is
empty implies not
a6 is
empty ) & ( not
a5 is
empty implies not
XOR2 b6,
(AND2 g6,a11) is
empty ) & ( not
XOR2 b6,
(AND2 g6,a11) is
empty implies not
a5 is
empty ) & ( not
a4 is
empty implies not
XOR2 b5,
(AND2 g5,a11) is
empty ) & ( not
XOR2 b5,
(AND2 g5,a11) is
empty implies not
a4 is
empty ) & ( not
a3 is
empty implies not
XOR2 b4,
(AND2 g4,a11) is
empty ) & ( not
XOR2 b4,
(AND2 g4,a11) is
empty implies not
a3 is
empty ) & ( not
a2 is
empty implies not
XOR2 b3,
(AND2 g3,a11) is
empty ) & ( not
XOR2 b3,
(AND2 g3,a11) is
empty implies not
a2 is
empty ) & ( not
a1 is
empty implies not
XOR2 b2,
(AND2 g2,a11) is
empty ) & ( not
XOR2 b2,
(AND2 g2,a11) is
empty implies not
a1 is
empty ) & ( not
a0 is
empty implies not
XOR2 b1,
(AND2 g1,a11) is
empty ) & ( not
XOR2 b1,
(AND2 g1,a11) is
empty implies not
a0 is
empty ) & ( not
p is
empty implies not
XOR2 b0,
(AND2 g0,a11) is
empty ) & ( not
XOR2 b0,
(AND2 g0,a11) is
empty implies not
p is
empty ) ) )
theorem
for
g0,
g1,
g2,
g3,
g4,
g5,
g6,
g7,
g8,
g9,
g10,
g11,
g12,
g13,
g14,
g15,
g16,
a0,
a1,
a2,
a3,
a4,
a5,
a6,
a7,
a8,
a9,
a10,
a11,
a12,
a13,
a14,
a15,
b0,
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
b12,
b13,
b14,
b15,
p being
set holds
not ( not
g16 is
empty & ( not
b0 is
empty implies not
XOR2 p,
(AND2 g0,a15) is
empty ) & ( not
XOR2 p,
(AND2 g0,a15) is
empty implies not
b0 is
empty ) & ( not
b1 is
empty implies not
XOR2 a0,
(AND2 g1,a15) is
empty ) & ( not
XOR2 a0,
(AND2 g1,a15) is
empty implies not
b1 is
empty ) & ( not
b2 is
empty implies not
XOR2 a1,
(AND2 g2,a15) is
empty ) & ( not
XOR2 a1,
(AND2 g2,a15) is
empty implies not
b2 is
empty ) & ( not
b3 is
empty implies not
XOR2 a2,
(AND2 g3,a15) is
empty ) & ( not
XOR2 a2,
(AND2 g3,a15) is
empty implies not
b3 is
empty ) & ( not
b4 is
empty implies not
XOR2 a3,
(AND2 g4,a15) is
empty ) & ( not
XOR2 a3,
(AND2 g4,a15) is
empty implies not
b4 is
empty ) & ( not
b5 is
empty implies not
XOR2 a4,
(AND2 g5,a15) is
empty ) & ( not
XOR2 a4,
(AND2 g5,a15) is
empty implies not
b5 is
empty ) & ( not
b6 is
empty implies not
XOR2 a5,
(AND2 g6,a15) is
empty ) & ( not
XOR2 a5,
(AND2 g6,a15) is
empty implies not
b6 is
empty ) & ( not
b7 is
empty implies not
XOR2 a6,
(AND2 g7,a15) is
empty ) & ( not
XOR2 a6,
(AND2 g7,a15) is
empty implies not
b7 is
empty ) & ( not
b8 is
empty implies not
XOR2 a7,
(AND2 g8,a15) is
empty ) & ( not
XOR2 a7,
(AND2 g8,a15) is
empty implies not
b8 is
empty ) & ( not
b9 is
empty implies not
XOR2 a8,
(AND2 g9,a15) is
empty ) & ( not
XOR2 a8,
(AND2 g9,a15) is
empty implies not
b9 is
empty ) & ( not
b10 is
empty implies not
XOR2 a9,
(AND2 g10,a15) is
empty ) & ( not
XOR2 a9,
(AND2 g10,a15) is
empty implies not
b10 is
empty ) & ( not
b11 is
empty implies not
XOR2 a10,
(AND2 g11,a15) is
empty ) & ( not
XOR2 a10,
(AND2 g11,a15) is
empty implies not
b11 is
empty ) & ( not
b12 is
empty implies not
XOR2 a11,
(AND2 g12,a15) is
empty ) & ( not
XOR2 a11,
(AND2 g12,a15) is
empty implies not
b12 is
empty ) & ( not
b13 is
empty implies not
XOR2 a12,
(AND2 g13,a15) is
empty ) & ( not
XOR2 a12,
(AND2 g13,a15) is
empty implies not
b13 is
empty ) & ( not
b14 is
empty implies not
XOR2 a13,
(AND2 g14,a15) is
empty ) & ( not
XOR2 a13,
(AND2 g14,a15) is
empty implies not
b14 is
empty ) & ( not
b15 is
empty implies not
XOR2 a14,
(AND2 g15,a15) is
empty ) & ( not
XOR2 a14,
(AND2 g15,a15) is
empty implies not
b15 is
empty ) & not ( ( not
a15 is
empty implies not
AND2 g16,
a15 is
empty ) & ( not
AND2 g16,
a15 is
empty implies not
a15 is
empty ) & ( not
a14 is
empty implies not
XOR2 b15,
(AND2 g15,a15) is
empty ) & ( not
XOR2 b15,
(AND2 g15,a15) is
empty implies not
a14 is
empty ) & ( not
a13 is
empty implies not
XOR2 b14,
(AND2 g14,a15) is
empty ) & ( not
XOR2 b14,
(AND2 g14,a15) is
empty implies not
a13 is
empty ) & ( not
a12 is
empty implies not
XOR2 b13,
(AND2 g13,a15) is
empty ) & ( not
XOR2 b13,
(AND2 g13,a15) is
empty implies not
a12 is
empty ) & ( not
a11 is
empty implies not
XOR2 b12,
(AND2 g12,a15) is
empty ) & ( not
XOR2 b12,
(AND2 g12,a15) is
empty implies not
a11 is
empty ) & ( not
a10 is
empty implies not
XOR2 b11,
(AND2 g11,a15) is
empty ) & ( not
XOR2 b11,
(AND2 g11,a15) is
empty implies not
a10 is
empty ) & ( not
a9 is
empty implies not
XOR2 b10,
(AND2 g10,a15) is
empty ) & ( not
XOR2 b10,
(AND2 g10,a15) is
empty implies not
a9 is
empty ) & ( not
a8 is
empty implies not
XOR2 b9,
(AND2 g9,a15) is
empty ) & ( not
XOR2 b9,
(AND2 g9,a15) is
empty implies not
a8 is
empty ) & ( not
a7 is
empty implies not
XOR2 b8,
(AND2 g8,a15) is
empty ) & ( not
XOR2 b8,
(AND2 g8,a15) is
empty implies not
a7 is
empty ) & ( not
a6 is
empty implies not
XOR2 b7,
(AND2 g7,a15) is
empty ) & ( not
XOR2 b7,
(AND2 g7,a15) is
empty implies not
a6 is
empty ) & ( not
a5 is
empty implies not
XOR2 b6,
(AND2 g6,a15) is
empty ) & ( not
XOR2 b6,
(AND2 g6,a15) is
empty implies not
a5 is
empty ) & ( not
a4 is
empty implies not
XOR2 b5,
(AND2 g5,a15) is
empty ) & ( not
XOR2 b5,
(AND2 g5,a15) is
empty implies not
a4 is
empty ) & ( not
a3 is
empty implies not
XOR2 b4,
(AND2 g4,a15) is
empty ) & ( not
XOR2 b4,
(AND2 g4,a15) is
empty implies not
a3 is
empty ) & ( not
a2 is
empty implies not
XOR2 b3,
(AND2 g3,a15) is
empty ) & ( not
XOR2 b3,
(AND2 g3,a15) is
empty implies not
a2 is
empty ) & ( not
a1 is
empty implies not
XOR2 b2,
(AND2 g2,a15) is
empty ) & ( not
XOR2 b2,
(AND2 g2,a15) is
empty implies not
a1 is
empty ) & ( not
a0 is
empty implies not
XOR2 b1,
(AND2 g1,a15) is
empty ) & ( not
XOR2 b1,
(AND2 g1,a15) is
empty implies not
a0 is
empty ) & ( not
p is
empty implies not
XOR2 b0,
(AND2 g0,a15) is
empty ) & ( not
XOR2 b0,
(AND2 g0,a15) is
empty implies not
p is
empty ) ) )
begin
theorem
for
g0,
g1,
g2,
g3,
g4,
g5,
g6,
g7,
g8,
g9,
g10,
g11,
g12,
a0,
a1,
a2,
a3,
a4,
a5,
a6,
a7,
a8,
a9,
a10,
a11,
b0,
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
z,
p being
set st not
g0 is
empty &
z is
empty & ( not
b0 is
empty implies not
XOR2 p,
a11 is
empty ) & ( not
XOR2 p,
a11 is
empty implies not
b0 is
empty ) & ( not
b1 is
empty implies not
XOR2 a0,
(AND2 g1,b0) is
empty ) & ( not
XOR2 a0,
(AND2 g1,b0) is
empty implies not
b1 is
empty ) & ( not
b2 is
empty implies not
XOR2 a1,
(AND2 g2,b0) is
empty ) & ( not
XOR2 a1,
(AND2 g2,b0) is
empty implies not
b2 is
empty ) & ( not
b3 is
empty implies not
XOR2 a2,
(AND2 g3,b0) is
empty ) & ( not
XOR2 a2,
(AND2 g3,b0) is
empty implies not
b3 is
empty ) & ( not
b4 is
empty implies not
XOR2 a3,
(AND2 g4,b0) is
empty ) & ( not
XOR2 a3,
(AND2 g4,b0) is
empty implies not
b4 is
empty ) & ( not
b5 is
empty implies not
XOR2 a4,
(AND2 g5,b0) is
empty ) & ( not
XOR2 a4,
(AND2 g5,b0) is
empty implies not
b5 is
empty ) & ( not
b6 is
empty implies not
XOR2 a5,
(AND2 g6,b0) is
empty ) & ( not
XOR2 a5,
(AND2 g6,b0) is
empty implies not
b6 is
empty ) & ( not
b7 is
empty implies not
XOR2 a6,
(AND2 g7,b0) is
empty ) & ( not
XOR2 a6,
(AND2 g7,b0) is
empty implies not
b7 is
empty ) & ( not
b8 is
empty implies not
XOR2 a7,
(AND2 g8,b0) is
empty ) & ( not
XOR2 a7,
(AND2 g8,b0) is
empty implies not
b8 is
empty ) & ( not
b9 is
empty implies not
XOR2 a8,
(AND2 g9,b0) is
empty ) & ( not
XOR2 a8,
(AND2 g9,b0) is
empty implies not
b9 is
empty ) & ( not
b10 is
empty implies not
XOR2 a9,
(AND2 g10,b0) is
empty ) & ( not
XOR2 a9,
(AND2 g10,b0) is
empty implies not
b10 is
empty ) & ( not
b11 is
empty implies not
XOR2 a10,
(AND2 g11,b0) is
empty ) & ( not
XOR2 a10,
(AND2 g11,b0) is
empty implies not
b11 is
empty ) holds
( ( not
b11 is
empty implies not
XOR2 (XOR2 a10,(AND2 g11,a11)),
(XOR2 z,(AND2 g11,p)) is
empty ) & ( not
XOR2 (XOR2 a10,(AND2 g11,a11)),
(XOR2 z,(AND2 g11,p)) is
empty implies not
b11 is
empty ) & ( not
b10 is
empty implies not
XOR2 (XOR2 a9,(AND2 g10,a11)),
(XOR2 z,(AND2 g10,p)) is
empty ) & ( not
XOR2 (XOR2 a9,(AND2 g10,a11)),
(XOR2 z,(AND2 g10,p)) is
empty implies not
b10 is
empty ) & ( not
b9 is
empty implies not
XOR2 (XOR2 a8,(AND2 g9,a11)),
(XOR2 z,(AND2 g9,p)) is
empty ) & ( not
XOR2 (XOR2 a8,(AND2 g9,a11)),
(XOR2 z,(AND2 g9,p)) is
empty implies not
b9 is
empty ) & ( not
b8 is
empty implies not
XOR2 (XOR2 a7,(AND2 g8,a11)),
(XOR2 z,(AND2 g8,p)) is
empty ) & ( not
XOR2 (XOR2 a7,(AND2 g8,a11)),
(XOR2 z,(AND2 g8,p)) is
empty implies not
b8 is
empty ) & ( not
b7 is
empty implies not
XOR2 (XOR2 a6,(AND2 g7,a11)),
(XOR2 z,(AND2 g7,p)) is
empty ) & ( not
XOR2 (XOR2 a6,(AND2 g7,a11)),
(XOR2 z,(AND2 g7,p)) is
empty implies not
b7 is
empty ) & ( not
b6 is
empty implies not
XOR2 (XOR2 a5,(AND2 g6,a11)),
(XOR2 z,(AND2 g6,p)) is
empty ) & ( not
XOR2 (XOR2 a5,(AND2 g6,a11)),
(XOR2 z,(AND2 g6,p)) is
empty implies not
b6 is
empty ) & ( not
b5 is
empty implies not
XOR2 (XOR2 a4,(AND2 g5,a11)),
(XOR2 z,(AND2 g5,p)) is
empty ) & ( not
XOR2 (XOR2 a4,(AND2 g5,a11)),
(XOR2 z,(AND2 g5,p)) is
empty implies not
b5 is
empty ) & ( not
b4 is
empty implies not
XOR2 (XOR2 a3,(AND2 g4,a11)),
(XOR2 z,(AND2 g4,p)) is
empty ) & ( not
XOR2 (XOR2 a3,(AND2 g4,a11)),
(XOR2 z,(AND2 g4,p)) is
empty implies not
b4 is
empty ) & ( not
b3 is
empty implies not
XOR2 (XOR2 a2,(AND2 g3,a11)),
(XOR2 z,(AND2 g3,p)) is
empty ) & ( not
XOR2 (XOR2 a2,(AND2 g3,a11)),
(XOR2 z,(AND2 g3,p)) is
empty implies not
b3 is
empty ) & ( not
b2 is
empty implies not
XOR2 (XOR2 a1,(AND2 g2,a11)),
(XOR2 z,(AND2 g2,p)) is
empty ) & ( not
XOR2 (XOR2 a1,(AND2 g2,a11)),
(XOR2 z,(AND2 g2,p)) is
empty implies not
b2 is
empty ) & ( not
b1 is
empty implies not
XOR2 (XOR2 a0,(AND2 g1,a11)),
(XOR2 z,(AND2 g1,p)) is
empty ) & ( not
XOR2 (XOR2 a0,(AND2 g1,a11)),
(XOR2 z,(AND2 g1,p)) is
empty implies not
b1 is
empty ) & ( not
b0 is
empty implies not
XOR2 (XOR2 z,(AND2 g0,a11)),
(XOR2 z,(AND2 g0,p)) is
empty ) & ( not
XOR2 (XOR2 z,(AND2 g0,a11)),
(XOR2 z,(AND2 g0,p)) is
empty implies not
b0 is
empty ) )
theorem
for
g0,
g1,
g2,
g3,
g4,
g5,
g6,
g7,
g8,
g9,
g10,
g11,
g12,
g13,
g14,
g15,
g16,
a0,
a1,
a2,
a3,
a4,
a5,
a6,
a7,
a8,
a9,
a10,
a11,
a12,
a13,
a14,
a15,
b0,
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
b12,
b13,
b14,
b15,
z,
p being
set st not
g0 is
empty &
z is
empty & ( not
b0 is
empty implies not
XOR2 p,
a15 is
empty ) & ( not
XOR2 p,
a15 is
empty implies not
b0 is
empty ) & ( not
b1 is
empty implies not
XOR2 a0,
(AND2 g1,b0) is
empty ) & ( not
XOR2 a0,
(AND2 g1,b0) is
empty implies not
b1 is
empty ) & ( not
b2 is
empty implies not
XOR2 a1,
(AND2 g2,b0) is
empty ) & ( not
XOR2 a1,
(AND2 g2,b0) is
empty implies not
b2 is
empty ) & ( not
b3 is
empty implies not
XOR2 a2,
(AND2 g3,b0) is
empty ) & ( not
XOR2 a2,
(AND2 g3,b0) is
empty implies not
b3 is
empty ) & ( not
b4 is
empty implies not
XOR2 a3,
(AND2 g4,b0) is
empty ) & ( not
XOR2 a3,
(AND2 g4,b0) is
empty implies not
b4 is
empty ) & ( not
b5 is
empty implies not
XOR2 a4,
(AND2 g5,b0) is
empty ) & ( not
XOR2 a4,
(AND2 g5,b0) is
empty implies not
b5 is
empty ) & ( not
b6 is
empty implies not
XOR2 a5,
(AND2 g6,b0) is
empty ) & ( not
XOR2 a5,
(AND2 g6,b0) is
empty implies not
b6 is
empty ) & ( not
b7 is
empty implies not
XOR2 a6,
(AND2 g7,b0) is
empty ) & ( not
XOR2 a6,
(AND2 g7,b0) is
empty implies not
b7 is
empty ) & ( not
b8 is
empty implies not
XOR2 a7,
(AND2 g8,b0) is
empty ) & ( not
XOR2 a7,
(AND2 g8,b0) is
empty implies not
b8 is
empty ) & ( not
b9 is
empty implies not
XOR2 a8,
(AND2 g9,b0) is
empty ) & ( not
XOR2 a8,
(AND2 g9,b0) is
empty implies not
b9 is
empty ) & ( not
b10 is
empty implies not
XOR2 a9,
(AND2 g10,b0) is
empty ) & ( not
XOR2 a9,
(AND2 g10,b0) is
empty implies not
b10 is
empty ) & ( not
b11 is
empty implies not
XOR2 a10,
(AND2 g11,b0) is
empty ) & ( not
XOR2 a10,
(AND2 g11,b0) is
empty implies not
b11 is
empty ) & ( not
b12 is
empty implies not
XOR2 a11,
(AND2 g12,b0) is
empty ) & ( not
XOR2 a11,
(AND2 g12,b0) is
empty implies not
b12 is
empty ) & ( not
b13 is
empty implies not
XOR2 a12,
(AND2 g13,b0) is
empty ) & ( not
XOR2 a12,
(AND2 g13,b0) is
empty implies not
b13 is
empty ) & ( not
b14 is
empty implies not
XOR2 a13,
(AND2 g14,b0) is
empty ) & ( not
XOR2 a13,
(AND2 g14,b0) is
empty implies not
b14 is
empty ) & ( not
b15 is
empty implies not
XOR2 a14,
(AND2 g15,b0) is
empty ) & ( not
XOR2 a14,
(AND2 g15,b0) is
empty implies not
b15 is
empty ) holds
( ( not
b15 is
empty implies not
XOR2 (XOR2 a14,(AND2 g15,a15)),
(XOR2 z,(AND2 g15,p)) is
empty ) & ( not
XOR2 (XOR2 a14,(AND2 g15,a15)),
(XOR2 z,(AND2 g15,p)) is
empty implies not
b15 is
empty ) & ( not
b14 is
empty implies not
XOR2 (XOR2 a13,(AND2 g14,a15)),
(XOR2 z,(AND2 g14,p)) is
empty ) & ( not
XOR2 (XOR2 a13,(AND2 g14,a15)),
(XOR2 z,(AND2 g14,p)) is
empty implies not
b14 is
empty ) & ( not
b13 is
empty implies not
XOR2 (XOR2 a12,(AND2 g13,a15)),
(XOR2 z,(AND2 g13,p)) is
empty ) & ( not
XOR2 (XOR2 a12,(AND2 g13,a15)),
(XOR2 z,(AND2 g13,p)) is
empty implies not
b13 is
empty ) & ( not
b12 is
empty implies not
XOR2 (XOR2 a11,(AND2 g12,a15)),
(XOR2 z,(AND2 g12,p)) is
empty ) & ( not
XOR2 (XOR2 a11,(AND2 g12,a15)),
(XOR2 z,(AND2 g12,p)) is
empty implies not
b12 is
empty ) & ( not
b11 is
empty implies not
XOR2 (XOR2 a10,(AND2 g11,a15)),
(XOR2 z,(AND2 g11,p)) is
empty ) & ( not
XOR2 (XOR2 a10,(AND2 g11,a15)),
(XOR2 z,(AND2 g11,p)) is
empty implies not
b11 is
empty ) & ( not
b10 is
empty implies not
XOR2 (XOR2 a9,(AND2 g10,a15)),
(XOR2 z,(AND2 g10,p)) is
empty ) & ( not
XOR2 (XOR2 a9,(AND2 g10,a15)),
(XOR2 z,(AND2 g10,p)) is
empty implies not
b10 is
empty ) & ( not
b9 is
empty implies not
XOR2 (XOR2 a8,(AND2 g9,a15)),
(XOR2 z,(AND2 g9,p)) is
empty ) & ( not
XOR2 (XOR2 a8,(AND2 g9,a15)),
(XOR2 z,(AND2 g9,p)) is
empty implies not
b9 is
empty ) & ( not
b8 is
empty implies not
XOR2 (XOR2 a7,(AND2 g8,a15)),
(XOR2 z,(AND2 g8,p)) is
empty ) & ( not
XOR2 (XOR2 a7,(AND2 g8,a15)),
(XOR2 z,(AND2 g8,p)) is
empty implies not
b8 is
empty ) & ( not
b7 is
empty implies not
XOR2 (XOR2 a6,(AND2 g7,a15)),
(XOR2 z,(AND2 g7,p)) is
empty ) & ( not
XOR2 (XOR2 a6,(AND2 g7,a15)),
(XOR2 z,(AND2 g7,p)) is
empty implies not
b7 is
empty ) & ( not
b6 is
empty implies not
XOR2 (XOR2 a5,(AND2 g6,a15)),
(XOR2 z,(AND2 g6,p)) is
empty ) & ( not
XOR2 (XOR2 a5,(AND2 g6,a15)),
(XOR2 z,(AND2 g6,p)) is
empty implies not
b6 is
empty ) & ( not
b5 is
empty implies not
XOR2 (XOR2 a4,(AND2 g5,a15)),
(XOR2 z,(AND2 g5,p)) is
empty ) & ( not
XOR2 (XOR2 a4,(AND2 g5,a15)),
(XOR2 z,(AND2 g5,p)) is
empty implies not
b5 is
empty ) & ( not
b4 is
empty implies not
XOR2 (XOR2 a3,(AND2 g4,a15)),
(XOR2 z,(AND2 g4,p)) is
empty ) & ( not
XOR2 (XOR2 a3,(AND2 g4,a15)),
(XOR2 z,(AND2 g4,p)) is
empty implies not
b4 is
empty ) & ( not
b3 is
empty implies not
XOR2 (XOR2 a2,(AND2 g3,a15)),
(XOR2 z,(AND2 g3,p)) is
empty ) & ( not
XOR2 (XOR2 a2,(AND2 g3,a15)),
(XOR2 z,(AND2 g3,p)) is
empty implies not
b3 is
empty ) & ( not
b2 is
empty implies not
XOR2 (XOR2 a1,(AND2 g2,a15)),
(XOR2 z,(AND2 g2,p)) is
empty ) & ( not
XOR2 (XOR2 a1,(AND2 g2,a15)),
(XOR2 z,(AND2 g2,p)) is
empty implies not
b2 is
empty ) & ( not
b1 is
empty implies not
XOR2 (XOR2 a0,(AND2 g1,a15)),
(XOR2 z,(AND2 g1,p)) is
empty ) & ( not
XOR2 (XOR2 a0,(AND2 g1,a15)),
(XOR2 z,(AND2 g1,p)) is
empty implies not
b1 is
empty ) & ( not
b0 is
empty implies not
XOR2 (XOR2 z,(AND2 g0,a15)),
(XOR2 z,(AND2 g0,p)) is
empty ) & ( not
XOR2 (XOR2 z,(AND2 g0,a15)),
(XOR2 z,(AND2 g0,p)) is
empty implies not
b0 is
empty ) )