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

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