for x0, x1, y0, y1, z0, z1, z2, z3, q00, q01, c01, q11, c11 being set holds
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 ) ) )