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 35;
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 36;
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