let x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03, q11, q12, q13, c11, c12, c13 be set ; :: thesis: not ( ( not q00 is empty implies not AND2 (x0,y0) is empty ) & ( not AND2 (x0,y0) is empty implies not q00 is empty ) & ( not q01 is empty implies not XOR3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) & ( not XOR3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty implies not q01 is empty ) & ( not c01 is empty implies not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) & ( not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty implies not c01 is empty ) & ( not q02 is empty implies not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty ) & ( not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty implies not q02 is empty ) & ( not c02 is empty implies not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty ) & ( not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty implies not c02 is empty ) & ( not q03 is empty implies not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty ) & ( not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty implies not q03 is empty ) & ( not c03 is empty implies not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty ) & ( not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty implies not c03 is empty ) & ( not q11 is empty implies not XOR3 (q02,c01,{}) is empty ) & ( not XOR3 (q02,c01,{}) is empty implies not q11 is empty ) & ( not c11 is empty implies not MAJ3 (q02,c01,{}) is empty ) & ( not MAJ3 (q02,c01,{}) is empty implies not c11 is empty ) & ( not q12 is empty implies not XOR3 (q03,c02,c11) is empty ) & ( not XOR3 (q03,c02,c11) is empty implies not q12 is empty ) & ( not c12 is empty implies not MAJ3 (q03,c02,c11) is empty ) & ( not MAJ3 (q03,c02,c11) is empty implies not c12 is empty ) & ( not q13 is empty implies not XOR3 ((AND2 (x2,y2)),c03,c12) is empty ) & ( not XOR3 ((AND2 (x2,y2)),c03,c12) is empty implies not q13 is empty ) & ( not c13 is empty implies not MAJ3 ((AND2 (x2,y2)),c03,c12) is empty ) & ( not MAJ3 ((AND2 (x2,y2)),c03,c12) is empty implies not c13 is empty ) & ( not z0 is empty implies not q00 is empty ) & ( not q00 is empty implies not z0 is empty ) & ( not z1 is empty implies not q01 is empty ) & ( not q01 is empty implies not z1 is empty ) & ( not z2 is empty implies not q11 is empty ) & ( not q11 is empty implies not z2 is empty ) & ( not z3 is empty implies not q12 is empty ) & ( not q12 is empty implies not z3 is empty ) & ( not z4 is empty implies not q13 is empty ) & ( not q13 is empty implies not z4 is empty ) & ( not z5 is empty implies not c13 is empty ) & ( not c13 is empty implies not z5 is empty ) & not ( ( not z0 is empty implies not MULT310 (x2,x1,y1,x0,y0) is empty ) & ( not MULT310 (x2,x1,y1,x0,y0) is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT311 (x2,x1,y1,x0,y0) is empty ) & ( not MULT311 (x2,x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) ) )
assume that
A1: ( not q00 is empty iff not AND2 (x0,y0) is empty ) and
A2: ( not q01 is empty iff not XOR3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) and
A3: ( not c01 is empty iff not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) and
A4: ( not q02 is empty iff not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty ) and
A5: ( not c02 is empty iff not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty ) and
A6: ( not q03 is empty iff not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty ) and
A7: ( not c03 is empty iff not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty ) and
A8: ( not q11 is empty iff not XOR3 (q02,c01,{}) is empty ) and
A9: ( not c11 is empty iff not MAJ3 (q02,c01,{}) is empty ) and
A10: ( not q12 is empty iff not XOR3 (q03,c02,c11) is empty ) and
A11: ( not c12 is empty iff not MAJ3 (q03,c02,c11) is empty ) and
A12: ( not q13 is empty iff not XOR3 ((AND2 (x2,y2)),c03,c12) is empty ) and
A13: ( not c13 is empty iff not MAJ3 ((AND2 (x2,y2)),c03,c12) is empty ) and
A14: ( not z0 is empty iff not q00 is empty ) and
A15: ( not z1 is empty iff not q01 is empty ) and
A16: ( not z2 is empty iff not q11 is empty ) and
A17: ( not z3 is empty iff not q12 is empty ) and
A18: ( not z4 is empty iff not q13 is empty ) and
A19: ( not z5 is empty iff not c13 is empty ) ; :: thesis: ( ( not z0 is empty implies not MULT310 (x2,x1,y1,x0,y0) is empty ) & ( not MULT310 (x2,x1,y1,x0,y0) is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT311 (x2,x1,y1,x0,y0) is empty ) & ( not MULT311 (x2,x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
thus ( not z0 is empty iff not MULT310 (x2,x1,y1,x0,y0) is empty ) by ; :: thesis: ( ( not z1 is empty implies not MULT311 (x2,x1,y1,x0,y0) is empty ) & ( not MULT311 (x2,x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
thus ( not z1 is empty iff not MULT311 (x2,x1,y1,x0,y0) is empty ) by ; :: thesis: ( ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
set m312 = MULT312 (x2,x1,y1,x0,y0);
set x0y2 = AND2 (x0,y2);
set x1y1 = AND2 (x1,y1);
set x0y1 = AND2 (x0,y1);
set x2y0 = AND2 (x2,y0);
set x1y0 = AND2 (x1,y0);
A20: MULT312 (x2,x1,y1,x0,y0) = XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}))) by GATE_1:def 35;
set m323 = MULT323 (x2,y2,x1,y1,x0,y0);
set m314 = MULT314 (x2,x1,y1,x0,y0);
set x2y2 = AND2 (x2,y2);
set m322 = MULT322 (x2,y2,x1,y1,x0,y0);
set m313 = MULT313 (x2,x1,y1,x0,y0);
set x1y2 = AND2 (x1,y2);
set x2y1 = AND2 (x2,y1);
A21: ( ( ( not AND2 (x2,y1) is empty & AND2 (x1,y2) is empty ) or ( AND2 (x2,y1) is empty & not AND2 (x1,y2) is empty ) ) iff not q03 is empty ) by A6;
A22: ( ( ( ( ( not AND2 (x2,y0) is empty & AND2 (x1,y1) is empty ) or ( AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) ) & AND2 (x0,y2) is empty ) or ( not ( not AND2 (x2,y0) is empty & AND2 (x1,y1) is empty ) & not ( AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) & not AND2 (x0,y2) is empty ) ) iff not q02 is empty ) by A4;
hence ( not z2 is empty iff not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A8, A16, A20; :: thesis: ( ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
A23: MULT313 (x2,x1,y1,x0,y0) = XOR3 ({},(AND2 (x2,y1)),(CARR2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}))) by GATE_1:def 37
.= XOR3 ({},(AND2 (x2,y1)),(MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}))))) by GATE_1:def 36 ;
MULT322 (x2,y2,x1,y1,x0,y0) = XOR3 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MAJ3 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}))) by GATE_1:def 35;
hence ( not z3 is empty iff not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A5, A9, A10, A17, A22, A21, A20, A23; :: thesis: ( ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
A24: MULT314 (x2,x1,y1,x0,y0) = MAJ3 ({},(AND2 (x2,y1)),(CARR2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}))) by GATE_1:def 38
.= MAJ3 ({},(AND2 (x2,y1)),(MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}))))) by GATE_1:def 36 ;
set m324 = MULT324 (x2,y2,x1,y1,x0,y0);
A25: MULT324 (x2,y2,x1,y1,x0,y0) = MAJ3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(CARR2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}))) by GATE_1:def 38
.= MAJ3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MAJ3 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MAJ3 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}))))) by GATE_1:def 36 ;
A26: MULT323 (x2,y2,x1,y1,x0,y0) = XOR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(CARR2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}))) by GATE_1:def 37
.= XOR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MAJ3 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MAJ3 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}))))) by GATE_1:def 36 ;
( ( ( ( ( not AND2 (x2,y2) is empty & c03 is empty ) or ( AND2 (x2,y2) is empty & not c03 is empty ) ) & c12 is empty ) or ( not ( not AND2 (x2,y2) is empty & c03 is empty ) & not ( AND2 (x2,y2) is empty & not c03 is empty ) & not c12 is empty ) ) iff not q13 is empty ) by A12;
hence ( not z4 is empty iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A5, A7, A9, A11, A18, A22, A21, A20, A23, A24, A26; :: thesis: ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
( ( ( not AND2 (x2,y2) is empty & not c03 is empty ) or ( not c03 is empty & not c12 is empty ) or ( not c12 is empty & not AND2 (x2,y2) is empty ) ) iff not c13 is empty ) by A13;
hence ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A5, A7, A9, A11, A19, A22, A21, A20, A23, A24, A25; :: thesis: verum