theorem :: GATE_5:4

for x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03 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 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 ) ) )