let x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03 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 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 CLAADD1 (q02,c01,{}) is empty ) & ( not CLAADD1 (q02,c01,{}) is empty implies not z2 is empty ) & ( not z3 is empty implies not CLAADD2 (q03,c02,q02,c01,{}) is empty ) & ( not CLAADD2 (q03,c02,q02,c01,{}) is empty implies not z3 is empty ) & ( not z4 is empty implies not CLAADD3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) & ( not CLAADD3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty implies not z4 is empty ) & ( not z5 is empty implies not CLACARR3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) & ( not CLACARR3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) 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 z0 is empty iff not q00 is empty ) and
A9: ( not z1 is empty iff not q01 is empty ) and
A10: ( not z2 is empty iff not CLAADD1 (q02,c01,{}) is empty ) and
A11: ( not z3 is empty iff not CLAADD2 (q03,c02,q02,c01,{}) is empty ) and
A12: ( not z4 is empty iff not CLAADD3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) and
A13: ( not z5 is empty iff not CLACARR3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) 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 ) )
set x0y2 = AND2 (x0,y2);
set x1y1 = AND2 (x1,y1);
set x2y0 = AND2 (x2,y0);
thus ( not z0 is empty iff not MULT310 (x2,x1,y1,x0,y0) is empty ) by A1, A8; :: 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 A2, A9; :: 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 x0y1 = AND2 (x0,y1);
set x1y0 = AND2 (x1,y0);
A14: 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;
then A15: ( ( ( ( ( not AND2 (x2,y0) is empty & AND2 (x1,y1) is empty ) or ( AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) ) & ( AND2 (x1,y0) is empty or AND2 (x0,y1) 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 (x1,y0) is empty & not AND2 (x0,y1) is empty ) ) iff not MULT312 (x2,x1,y1,x0,y0) is empty ) ;
set x1y2 = AND2 (x1,y2);
set x2y1 = AND2 (x2,y1);
A16: ( ( ( 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;
set m324 = MULT324 (x2,y2,x1,y1,x0,y0);
set m323 = MULT323 (x2,y2,x1,y1,x0,y0);
set m314 = MULT314 (x2,x1,y1,x0,y0);
set x2y2 = AND2 (x2,y2);
A17: 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 m322 = MULT322 (x2,y2,x1,y1,x0,y0);
set m313 = MULT313 (x2,x1,y1,x0,y0);
A18: 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 ;
( ( ( ( ( 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, A10, A14; :: 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 ) )
A19: ( ( ( not AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) or ( not AND2 (x1,y1) is empty & not AND2 (x0,y2) is empty ) or ( not AND2 (x0,y2) is empty & not AND2 (x2,y0) is empty ) ) iff not c02 is empty ) by A5;
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;
then ( ( ( ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & AND2 (x1,y2) is empty ) or ( MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) ) & ( MULT312 (x2,x1,y1,x0,y0) is empty or AND2 (x0,y2) is empty ) ) or ( not ( not MULT313 (x2,x1,y1,x0,y0) is empty & AND2 (x1,y2) is empty ) & not ( MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) ) iff not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) ;
hence ( not z3 is empty iff not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A4, A11, A19, A16, A15, A18; :: 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 ) )
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 ;
then ( ( ( ( ( not MULT314 (x2,x1,y1,x0,y0) is empty & AND2 (x2,y2) is empty ) or ( MULT314 (x2,x1,y1,x0,y0) is empty & not AND2 (x2,y2) is empty ) ) & not ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) & not ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) & not ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) or ( not ( not MULT314 (x2,x1,y1,x0,y0) is empty & AND2 (x2,y2) is empty ) & not ( MULT314 (x2,x1,y1,x0,y0) is empty & not AND2 (x2,y2) is empty ) & ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) or ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) or ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) ) ) iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) ;
hence ( not z4 is empty iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A4, A7, A12, A19, A16, A15, A18, A17; :: thesis: ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
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 ;
then ( ( ( not MULT314 (x2,x1,y1,x0,y0) is empty & not AND2 (x2,y2) is empty ) or ( not AND2 (x2,y2) is empty & ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) or ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) or ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) ) or ( ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) or ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) or ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) & not MULT314 (x2,x1,y1,x0,y0) is empty ) ) iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) ;
hence ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A4, A7, A13, A19, A16, A15, A18, A17; :: thesis: verum