let 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 be set ; 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 ) ) )
assume that
A1:
not g16 is empty
and
A2:
( not b0 is empty iff not XOR2 p,(AND2 g0,a15) is empty )
and
A3:
( not b1 is empty iff not XOR2 a0,(AND2 g1,a15) is empty )
and
A4:
( not b2 is empty iff not XOR2 a1,(AND2 g2,a15) is empty )
and
A5:
( not b3 is empty iff not XOR2 a2,(AND2 g3,a15) is empty )
and
A6:
( not b4 is empty iff not XOR2 a3,(AND2 g4,a15) is empty )
and
A7:
( not b5 is empty iff not XOR2 a4,(AND2 g5,a15) is empty )
and
A8:
( not b6 is empty iff not XOR2 a5,(AND2 g6,a15) is empty )
and
A9:
( not b7 is empty iff not XOR2 a6,(AND2 g7,a15) is empty )
and
A10:
( not b8 is empty iff not XOR2 a7,(AND2 g8,a15) is empty )
and
A11:
( not b9 is empty iff not XOR2 a8,(AND2 g9,a15) is empty )
and
A12:
( not b10 is empty iff not XOR2 a9,(AND2 g10,a15) is empty )
and
A13:
( not b11 is empty iff not XOR2 a10,(AND2 g11,a15) is empty )
and
A14:
( not b12 is empty iff not XOR2 a11,(AND2 g12,a15) is empty )
and
A15:
( not b13 is empty iff not XOR2 a12,(AND2 g13,a15) is empty )
and
A16:
( not b14 is empty iff not XOR2 a13,(AND2 g14,a15) is empty )
and
A17:
( not b15 is empty iff not XOR2 a14,(AND2 g15,a15) is empty )
; ( ( 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 ) )
thus
( not a15 is empty iff not AND2 g16,a15 is empty )
by A1; ( ( 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 ) )
( ( ( not b15 is empty & AND2 g15,a15 is empty ) or ( b15 is empty & not AND2 g15,a15 is empty ) ) iff not XOR2 b15,(AND2 g15,a15) is empty )
;
hence
( not a14 is empty iff not XOR2 b15,(AND2 g15,a15) is empty )
by A17; ( ( 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 ) )
( ( ( not b14 is empty & AND2 g14,a15 is empty ) or ( b14 is empty & not AND2 g14,a15 is empty ) ) iff not XOR2 b14,(AND2 g14,a15) is empty )
;
hence
( not a13 is empty iff not XOR2 b14,(AND2 g14,a15) is empty )
by A16; ( ( 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 ) )
( ( ( not b13 is empty & AND2 g13,a15 is empty ) or ( b13 is empty & not AND2 g13,a15 is empty ) ) iff not XOR2 b13,(AND2 g13,a15) is empty )
;
hence
( not a12 is empty iff not XOR2 b13,(AND2 g13,a15) is empty )
by A15; ( ( 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 ) )
( ( ( not b12 is empty & AND2 g12,a15 is empty ) or ( b12 is empty & not AND2 g12,a15 is empty ) ) iff not XOR2 b12,(AND2 g12,a15) is empty )
;
hence
( not a11 is empty iff not XOR2 b12,(AND2 g12,a15) is empty )
by A14; ( ( 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 ) )
( ( ( not b11 is empty & AND2 g11,a15 is empty ) or ( b11 is empty & not AND2 g11,a15 is empty ) ) iff not XOR2 b11,(AND2 g11,a15) is empty )
;
hence
( not a10 is empty iff not XOR2 b11,(AND2 g11,a15) is empty )
by A13; ( ( 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 ) )
( ( ( not b10 is empty & AND2 g10,a15 is empty ) or ( b10 is empty & not AND2 g10,a15 is empty ) ) iff not XOR2 b10,(AND2 g10,a15) is empty )
;
hence
( not a9 is empty iff not XOR2 b10,(AND2 g10,a15) is empty )
by A12; ( ( 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 ) )
( ( ( not b9 is empty & AND2 g9,a15 is empty ) or ( b9 is empty & not AND2 g9,a15 is empty ) ) iff not XOR2 b9,(AND2 g9,a15) is empty )
;
hence
( not a8 is empty iff not XOR2 b9,(AND2 g9,a15) is empty )
by A11; ( ( 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 ) )
( ( ( not b8 is empty & AND2 g8,a15 is empty ) or ( b8 is empty & not AND2 g8,a15 is empty ) ) iff not XOR2 b8,(AND2 g8,a15) is empty )
;
hence
( not a7 is empty iff not XOR2 b8,(AND2 g8,a15) is empty )
by A10; ( ( 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 ) )
( ( ( not b7 is empty & AND2 g7,a15 is empty ) or ( b7 is empty & not AND2 g7,a15 is empty ) ) iff not XOR2 b7,(AND2 g7,a15) is empty )
;
hence
( not a6 is empty iff not XOR2 b7,(AND2 g7,a15) is empty )
by A9; ( ( 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 ) )
( ( ( not b6 is empty & AND2 g6,a15 is empty ) or ( b6 is empty & not AND2 g6,a15 is empty ) ) iff not XOR2 b6,(AND2 g6,a15) is empty )
;
hence
( not a5 is empty iff not XOR2 b6,(AND2 g6,a15) is empty )
by A8; ( ( 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 ) )
( ( ( not b5 is empty & AND2 g5,a15 is empty ) or ( b5 is empty & not AND2 g5,a15 is empty ) ) iff not XOR2 b5,(AND2 g5,a15) is empty )
;
hence
( not a4 is empty iff not XOR2 b5,(AND2 g5,a15) is empty )
by A7; ( ( 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 ) )
( ( ( not b4 is empty & AND2 g4,a15 is empty ) or ( b4 is empty & not AND2 g4,a15 is empty ) ) iff not XOR2 b4,(AND2 g4,a15) is empty )
;
hence
( not a3 is empty iff not XOR2 b4,(AND2 g4,a15) is empty )
by A6; ( ( 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 ) )
( ( ( not b3 is empty & AND2 g3,a15 is empty ) or ( b3 is empty & not AND2 g3,a15 is empty ) ) iff not XOR2 b3,(AND2 g3,a15) is empty )
;
hence
( not a2 is empty iff not XOR2 b3,(AND2 g3,a15) is empty )
by A5; ( ( 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 ) )
( ( ( not b2 is empty & AND2 g2,a15 is empty ) or ( b2 is empty & not AND2 g2,a15 is empty ) ) iff not XOR2 b2,(AND2 g2,a15) is empty )
;
hence
( not a1 is empty iff not XOR2 b2,(AND2 g2,a15) is empty )
by A4; ( ( 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 ) )
( ( ( not b1 is empty & AND2 g1,a15 is empty ) or ( b1 is empty & not AND2 g1,a15 is empty ) ) iff not XOR2 b1,(AND2 g1,a15) is empty )
;
hence
( not a0 is empty iff not XOR2 b1,(AND2 g1,a15) is empty )
by A3; ( not p is empty iff not XOR2 b0,(AND2 g0,a15) is empty )
( ( ( not b0 is empty & AND2 g0,a15 is empty ) or ( b0 is empty & not AND2 g0,a15 is empty ) ) iff not XOR2 b0,(AND2 g0,a15) is empty )
;
hence
( not p is empty iff not XOR2 b0,(AND2 g0,a15) is empty )
by A2; verum