:: GATE_4 semantic presentation

begin

theorem :: GATE_4:1
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 ) ) )
proof
let 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 be set ; ::_thesis: 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 ) ) )
assume that
A1: not g12 is empty and
A2: ( not b0 is empty iff not XOR2 (p,(AND2 (g0,a11))) is empty ) and
A3: ( not b1 is empty iff not XOR2 (a0,(AND2 (g1,a11))) is empty ) and
A4: ( not b2 is empty iff not XOR2 (a1,(AND2 (g2,a11))) is empty ) and
A5: ( not b3 is empty iff not XOR2 (a2,(AND2 (g3,a11))) is empty ) and
A6: ( not b4 is empty iff not XOR2 (a3,(AND2 (g4,a11))) is empty ) and
A7: ( not b5 is empty iff not XOR2 (a4,(AND2 (g5,a11))) is empty ) and
A8: ( not b6 is empty iff not XOR2 (a5,(AND2 (g6,a11))) is empty ) and
A9: ( not b7 is empty iff not XOR2 (a6,(AND2 (g7,a11))) is empty ) and
A10: ( not b8 is empty iff not XOR2 (a7,(AND2 (g8,a11))) is empty ) and
A11: ( not b9 is empty iff not XOR2 (a8,(AND2 (g9,a11))) is empty ) and
A12: ( not b10 is empty iff not XOR2 (a9,(AND2 (g10,a11))) is empty ) and
A13: ( not b11 is empty iff not XOR2 (a10,(AND2 (g11,a11))) is empty ) ; ::_thesis: ( ( 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 ) )
thus  ( not a11 is empty iff not AND2 (g12,a11) is empty ) by A1; ::_thesis: ( ( 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 ) )
 ( ( ( not b11 is empty & AND2 (g11,a11) is empty ) or ( b11 is empty & not AND2 (g11,a11) is empty ) ) iff not XOR2 (b11,(AND2 (g11,a11))) is empty ) ;
hence  ( not a10 is empty iff not XOR2 (b11,(AND2 (g11,a11))) is empty ) by A13; ::_thesis: ( ( 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 ) )
 ( ( ( not b10 is empty & AND2 (g10,a11) is empty ) or ( b10 is empty & not AND2 (g10,a11) is empty ) ) iff not XOR2 (b10,(AND2 (g10,a11))) is empty ) ;
hence  ( not a9 is empty iff not XOR2 (b10,(AND2 (g10,a11))) is empty ) by A12; ::_thesis: ( ( 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 ) )
 ( ( ( not b9 is empty & AND2 (g9,a11) is empty ) or ( b9 is empty & not AND2 (g9,a11) is empty ) ) iff not XOR2 (b9,(AND2 (g9,a11))) is empty ) ;
hence  ( not a8 is empty iff not XOR2 (b9,(AND2 (g9,a11))) is empty ) by A11; ::_thesis: ( ( 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 ) )
 ( ( ( not b8 is empty & AND2 (g8,a11) is empty ) or ( b8 is empty & not AND2 (g8,a11) is empty ) ) iff not XOR2 (b8,(AND2 (g8,a11))) is empty ) ;
hence  ( not a7 is empty iff not XOR2 (b8,(AND2 (g8,a11))) is empty ) by A10; ::_thesis: ( ( 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 ) )
 ( ( ( not b7 is empty & AND2 (g7,a11) is empty ) or ( b7 is empty & not AND2 (g7,a11) is empty ) ) iff not XOR2 (b7,(AND2 (g7,a11))) is empty ) ;
hence  ( not a6 is empty iff not XOR2 (b7,(AND2 (g7,a11))) is empty ) by A9; ::_thesis: ( ( 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 ) )
 ( ( ( not b6 is empty & AND2 (g6,a11) is empty ) or ( b6 is empty & not AND2 (g6,a11) is empty ) ) iff not XOR2 (b6,(AND2 (g6,a11))) is empty ) ;
hence  ( not a5 is empty iff not XOR2 (b6,(AND2 (g6,a11))) is empty ) by A8; ::_thesis: ( ( 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 ) )
 ( ( ( not b5 is empty & AND2 (g5,a11) is empty ) or ( b5 is empty & not AND2 (g5,a11) is empty ) ) iff not XOR2 (b5,(AND2 (g5,a11))) is empty ) ;
hence  ( not a4 is empty iff not XOR2 (b5,(AND2 (g5,a11))) is empty ) by A7; ::_thesis: ( ( 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 ) )
 ( ( ( not b4 is empty & AND2 (g4,a11) is empty ) or ( b4 is empty & not AND2 (g4,a11) is empty ) ) iff not XOR2 (b4,(AND2 (g4,a11))) is empty ) ;
hence  ( not a3 is empty iff not XOR2 (b4,(AND2 (g4,a11))) is empty ) by A6; ::_thesis: ( ( 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 ) )
 ( ( ( not b3 is empty & AND2 (g3,a11) is empty ) or ( b3 is empty & not AND2 (g3,a11) is empty ) ) iff not XOR2 (b3,(AND2 (g3,a11))) is empty ) ;
hence  ( not a2 is empty iff not XOR2 (b3,(AND2 (g3,a11))) is empty ) by A5; ::_thesis: ( ( 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 ) )
 ( ( ( not b2 is empty & AND2 (g2,a11) is empty ) or ( b2 is empty & not AND2 (g2,a11) is empty ) ) iff not XOR2 (b2,(AND2 (g2,a11))) is empty ) ;
hence  ( not a1 is empty iff not XOR2 (b2,(AND2 (g2,a11))) is empty ) by A4; ::_thesis: ( ( 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 ) )
 ( ( ( not b1 is empty & AND2 (g1,a11) is empty ) or ( b1 is empty & not AND2 (g1,a11) is empty ) ) iff not XOR2 (b1,(AND2 (g1,a11))) is empty ) ;
hence  ( not a0 is empty iff not XOR2 (b1,(AND2 (g1,a11))) is empty ) by A3; ::_thesis: ( not p is empty iff not XOR2 (b0,(AND2 (g0,a11))) is empty )
 ( ( ( not b0 is empty & AND2 (g0,a11) is empty ) or ( b0 is empty & not AND2 (g0,a11) is empty ) ) iff not XOR2 (b0,(AND2 (g0,a11))) is empty ) ;
hence  ( not p is empty iff not XOR2 (b0,(AND2 (g0,a11))) is empty ) by A2; ::_thesis: verum
end;

theorem :: GATE_4:2
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 ) ) )
proof
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 ; ::_thesis: 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 ) ; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( 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; ::_thesis: verum
end;

begin

theorem :: GATE_4:3
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 ) )
proof
let 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 be set ; ::_thesis: ( 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 ) implies ( ( 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 ) ) )
assume that
A1: not g0 is empty and
A2: z is empty and
A3: ( not b0 is empty iff not XOR2 (p,a11) is empty ) and
A4: ( not b1 is empty iff not XOR2 (a0,(AND2 (g1,b0))) is empty ) and
A5: ( not b2 is empty iff not XOR2 (a1,(AND2 (g2,b0))) is empty ) and
A6: ( not b3 is empty iff not XOR2 (a2,(AND2 (g3,b0))) is empty ) and
A7: ( not b4 is empty iff not XOR2 (a3,(AND2 (g4,b0))) is empty ) and
A8: ( not b5 is empty iff not XOR2 (a4,(AND2 (g5,b0))) is empty ) and
A9: ( not b6 is empty iff not XOR2 (a5,(AND2 (g6,b0))) is empty ) and
A10: ( not b7 is empty iff not XOR2 (a6,(AND2 (g7,b0))) is empty ) and
A11: ( not b8 is empty iff not XOR2 (a7,(AND2 (g8,b0))) is empty ) and
A12: ( not b9 is empty iff not XOR2 (a8,(AND2 (g9,b0))) is empty ) and
A13: ( not b10 is empty iff not XOR2 (a9,(AND2 (g10,b0))) is empty ) and
A14: ( not b11 is empty iff not XOR2 (a10,(AND2 (g11,b0))) is empty ) ; ::_thesis: ( ( 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 ) )
 ( ( ( not a10 is empty & ( g11 is empty or a11 is empty ) & ( g11 is empty or p is empty ) ) or ( a10 is empty & not g11 is empty & not a11 is empty & ( g11 is empty or p is empty ) ) or ( ( a10 is empty or ( not g11 is empty & not a11 is empty ) ) & ( not a10 is empty or g11 is empty or a11 is empty ) & not g11 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a10,(AND2 (g11,a11)))),(XOR2 (z,(AND2 (g11,p))))) is empty ) by A2;
hence  ( not b11 is empty iff not XOR2 ((XOR2 (a10,(AND2 (g11,a11)))),(XOR2 (z,(AND2 (g11,p))))) is empty ) by A3, A14; ::_thesis: ( ( 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 ) )
 ( ( ( not a9 is empty & ( g10 is empty or a11 is empty ) & ( g10 is empty or p is empty ) ) or ( a9 is empty & not g10 is empty & not a11 is empty & ( g10 is empty or p is empty ) ) or ( ( a9 is empty or ( not g10 is empty & not a11 is empty ) ) & ( not a9 is empty or g10 is empty or a11 is empty ) & not g10 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a9,(AND2 (g10,a11)))),(XOR2 (z,(AND2 (g10,p))))) is empty ) by A2;
hence  ( not b10 is empty iff not XOR2 ((XOR2 (a9,(AND2 (g10,a11)))),(XOR2 (z,(AND2 (g10,p))))) is empty ) by A3, A13; ::_thesis: ( ( 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 ) )
 ( ( ( not a8 is empty & ( g9 is empty or a11 is empty ) & ( g9 is empty or p is empty ) ) or ( a8 is empty & not g9 is empty & not a11 is empty & ( g9 is empty or p is empty ) ) or ( ( a8 is empty or ( not g9 is empty & not a11 is empty ) ) & ( not a8 is empty or g9 is empty or a11 is empty ) & not g9 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a8,(AND2 (g9,a11)))),(XOR2 (z,(AND2 (g9,p))))) is empty ) by A2;
hence  ( not b9 is empty iff not XOR2 ((XOR2 (a8,(AND2 (g9,a11)))),(XOR2 (z,(AND2 (g9,p))))) is empty ) by A3, A12; ::_thesis: ( ( 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 ) )
 ( ( ( not a7 is empty & ( g8 is empty or a11 is empty ) & ( g8 is empty or p is empty ) ) or ( a7 is empty & not g8 is empty & not a11 is empty & ( g8 is empty or p is empty ) ) or ( ( a7 is empty or ( not g8 is empty & not a11 is empty ) ) & ( not a7 is empty or g8 is empty or a11 is empty ) & not g8 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a7,(AND2 (g8,a11)))),(XOR2 (z,(AND2 (g8,p))))) is empty ) by A2;
hence  ( not b8 is empty iff not XOR2 ((XOR2 (a7,(AND2 (g8,a11)))),(XOR2 (z,(AND2 (g8,p))))) is empty ) by A3, A11; ::_thesis: ( ( 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 ) )
 ( ( ( not a6 is empty & ( g7 is empty or a11 is empty ) & ( g7 is empty or p is empty ) ) or ( a6 is empty & not g7 is empty & not a11 is empty & ( g7 is empty or p is empty ) ) or ( ( a6 is empty or ( not g7 is empty & not a11 is empty ) ) & ( not a6 is empty or g7 is empty or a11 is empty ) & not g7 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a6,(AND2 (g7,a11)))),(XOR2 (z,(AND2 (g7,p))))) is empty ) by A2;
hence  ( not b7 is empty iff not XOR2 ((XOR2 (a6,(AND2 (g7,a11)))),(XOR2 (z,(AND2 (g7,p))))) is empty ) by A3, A10; ::_thesis: ( ( 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 ) )
 ( ( ( not a5 is empty & ( g6 is empty or a11 is empty ) & ( g6 is empty or p is empty ) ) or ( a5 is empty & not g6 is empty & not a11 is empty & ( g6 is empty or p is empty ) ) or ( ( a5 is empty or ( not g6 is empty & not a11 is empty ) ) & ( not a5 is empty or g6 is empty or a11 is empty ) & not g6 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a5,(AND2 (g6,a11)))),(XOR2 (z,(AND2 (g6,p))))) is empty ) by A2;
hence  ( not b6 is empty iff not XOR2 ((XOR2 (a5,(AND2 (g6,a11)))),(XOR2 (z,(AND2 (g6,p))))) is empty ) by A3, A9; ::_thesis: ( ( 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 ) )
 ( ( ( not a4 is empty & ( g5 is empty or a11 is empty ) & ( g5 is empty or p is empty ) ) or ( a4 is empty & not g5 is empty & not a11 is empty & ( g5 is empty or p is empty ) ) or ( ( a4 is empty or ( not g5 is empty & not a11 is empty ) ) & ( not a4 is empty or g5 is empty or a11 is empty ) & not g5 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a4,(AND2 (g5,a11)))),(XOR2 (z,(AND2 (g5,p))))) is empty ) by A2;
hence  ( not b5 is empty iff not XOR2 ((XOR2 (a4,(AND2 (g5,a11)))),(XOR2 (z,(AND2 (g5,p))))) is empty ) by A3, A8; ::_thesis: ( ( 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 ) )
 ( ( ( not a3 is empty & ( g4 is empty or a11 is empty ) & ( g4 is empty or p is empty ) ) or ( a3 is empty & not g4 is empty & not a11 is empty & ( g4 is empty or p is empty ) ) or ( ( a3 is empty or ( not g4 is empty & not a11 is empty ) ) & ( not a3 is empty or g4 is empty or a11 is empty ) & not g4 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a3,(AND2 (g4,a11)))),(XOR2 (z,(AND2 (g4,p))))) is empty ) by A2;
hence  ( not b4 is empty iff not XOR2 ((XOR2 (a3,(AND2 (g4,a11)))),(XOR2 (z,(AND2 (g4,p))))) is empty ) by A3, A7; ::_thesis: ( ( 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 ) )
 ( ( ( not a2 is empty & ( g3 is empty or a11 is empty ) & ( g3 is empty or p is empty ) ) or ( a2 is empty & not g3 is empty & not a11 is empty & ( g3 is empty or p is empty ) ) or ( ( a2 is empty or ( not g3 is empty & not a11 is empty ) ) & ( not a2 is empty or g3 is empty or a11 is empty ) & not g3 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a2,(AND2 (g3,a11)))),(XOR2 (z,(AND2 (g3,p))))) is empty ) by A2;
hence  ( not b3 is empty iff not XOR2 ((XOR2 (a2,(AND2 (g3,a11)))),(XOR2 (z,(AND2 (g3,p))))) is empty ) by A3, A6; ::_thesis: ( ( 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 ) )
 ( ( ( not a1 is empty & ( g2 is empty or a11 is empty ) & ( g2 is empty or p is empty ) ) or ( a1 is empty & not g2 is empty & not a11 is empty & ( g2 is empty or p is empty ) ) or ( ( a1 is empty or ( not g2 is empty & not a11 is empty ) ) & ( not a1 is empty or g2 is empty or a11 is empty ) & not g2 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a1,(AND2 (g2,a11)))),(XOR2 (z,(AND2 (g2,p))))) is empty ) by A2;
hence  ( not b2 is empty iff not XOR2 ((XOR2 (a1,(AND2 (g2,a11)))),(XOR2 (z,(AND2 (g2,p))))) is empty ) by A3, A5; ::_thesis: ( ( 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 ) )
 ( ( ( not a0 is empty & ( g1 is empty or a11 is empty ) & ( g1 is empty or p is empty ) ) or ( a0 is empty & not g1 is empty & not a11 is empty & ( g1 is empty or p is empty ) ) or ( ( a0 is empty or ( not g1 is empty & not a11 is empty ) ) & ( not a0 is empty or g1 is empty or a11 is empty ) & not g1 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (a0,(AND2 (g1,a11)))),(XOR2 (z,(AND2 (g1,p))))) is empty ) by A2;
hence  ( not b1 is empty iff not XOR2 ((XOR2 (a0,(AND2 (g1,a11)))),(XOR2 (z,(AND2 (g1,p))))) is empty ) by A3, A4; ::_thesis: ( not b0 is empty iff not XOR2 ((XOR2 (z,(AND2 (g0,a11)))),(XOR2 (z,(AND2 (g0,p))))) is empty )
 ( ( ( not z is empty & ( g0 is empty or a11 is empty ) & ( g0 is empty or p is empty ) ) or ( z is empty & not g0 is empty & not a11 is empty & ( g0 is empty or p is empty ) ) or ( ( z is empty or ( not g0 is empty & not a11 is empty ) ) & ( not z is empty or g0 is empty or a11 is empty ) & not g0 is empty & not p is empty ) ) iff not XOR2 ((XOR2 (z,(AND2 (g0,a11)))),(XOR2 (z,(AND2 (g0,p))))) is empty ) by A2;
hence  ( not b0 is empty iff not XOR2 ((XOR2 (z,(AND2 (g0,a11)))),(XOR2 (z,(AND2 (g0,p))))) is empty ) by A1, A3; ::_thesis: verum
end;

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