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