let x0, x1, y0, y1, z0, z1, z2, z3, q00, q01, c01, q11, c11 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 q11 is empty implies not XOR3 (AND2 x1,y1),{} ,c01 is empty ) & ( not XOR3 (AND2 x1,y1),{} ,c01 is empty implies not q11 is empty ) & ( not c11 is empty implies not MAJ3 (AND2 x1,y1),{} ,c01 is empty ) & ( not MAJ3 (AND2 x1,y1),{} ,c01 is empty implies not c11 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 c11 is empty ) & ( not c11 is empty implies not z3 is empty ) & not ( ( not z0 is empty implies not MULT210 x1,y1,x0,y0 is empty ) & ( not MULT210 x1,y1,x0,y0 is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT211 x1,y1,x0,y0 is empty ) & ( not MULT211 x1,y1,x0,y0 is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT212 x1,y1,x0,y0 is empty ) & ( not MULT212 x1,y1,x0,y0 is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT213 x1,y1,x0,y0 is empty ) & ( not MULT213 x1,y1,x0,y0 is empty implies not z3 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 q11 is empty iff not XOR3 (AND2 x1,y1),{} ,c01 is empty ) and
A5: ( not c11 is empty iff not MAJ3 (AND2 x1,y1),{} ,c01 is empty ) and
A6: ( not z0 is empty iff not q00 is empty ) and
A7: ( not z1 is empty iff not q01 is empty ) and
A8: ( not z2 is empty iff not q11 is empty ) and
A9: ( not z3 is empty iff not c11 is empty ) ; :: thesis: ( ( not z0 is empty implies not MULT210 x1,y1,x0,y0 is empty ) & ( not MULT210 x1,y1,x0,y0 is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT211 x1,y1,x0,y0 is empty ) & ( not MULT211 x1,y1,x0,y0 is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT212 x1,y1,x0,y0 is empty ) & ( not MULT212 x1,y1,x0,y0 is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT213 x1,y1,x0,y0 is empty ) & ( not MULT213 x1,y1,x0,y0 is empty implies not z3 is empty ) )
thus ( not z0 is empty iff not MULT210 x1,y1,x0,y0 is empty ) by A1, A6; :: thesis: ( ( not z1 is empty implies not MULT211 x1,y1,x0,y0 is empty ) & ( not MULT211 x1,y1,x0,y0 is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT212 x1,y1,x0,y0 is empty ) & ( not MULT212 x1,y1,x0,y0 is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT213 x1,y1,x0,y0 is empty ) & ( not MULT213 x1,y1,x0,y0 is empty implies not z3 is empty ) )
thus ( not z1 is empty iff not MULT211 x1,y1,x0,y0 is empty ) by A2, A7; :: thesis: ( ( not z2 is empty implies not MULT212 x1,y1,x0,y0 is empty ) & ( not MULT212 x1,y1,x0,y0 is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT213 x1,y1,x0,y0 is empty ) & ( not MULT213 x1,y1,x0,y0 is empty implies not z3 is empty ) )
set m212 = MULT212 x1,y1,x0,y0;
set x1y1 = AND2 x1,y1;
set x0y1 = AND2 x0,y1;
set x1y0 = AND2 x1,y0;
MULT212 x1,y1,x0,y0 = XOR3 {} ,(AND2 x1,y1),(MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} ) by GATE_1:def 37;
then ( ( ( not AND2 x1,y1 is empty & MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} is empty ) or ( AND2 x1,y1 is empty & not MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} is empty ) ) iff not MULT212 x1,y1,x0,y0 is empty ) ;
hence ( not z2 is empty iff not MULT212 x1,y1,x0,y0 is empty ) by A3, A4, A8; :: thesis: ( not z3 is empty iff not MULT213 x1,y1,x0,y0 is empty )
set m213 = MULT213 x1,y1,x0,y0;
MULT213 x1,y1,x0,y0 = MAJ3 {} ,(AND2 x1,y1),(MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} ) by GATE_1:def 38;
then ( not MULT213 x1,y1,x0,y0 is empty iff ( not AND2 x1,y1 is empty & not MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} is empty ) ) ;
hence ( not z3 is empty iff not MULT213 x1,y1,x0,y0 is empty ) by A3, A5, A9; :: thesis: verum