:: GATE_5 semantic presentation begin definitionlet "x0", "x1", "y0", "y1" be ($#m1_hidden :::"set"::: ) ; func :::"MULT210"::: "(" "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 1 (Set ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y0" ")" ); func :::"MULT211"::: "(" "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 2 (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT212"::: "(" "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 3 (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT213"::: "(" "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 4 (Set ($#k36_gate_1 :::"CARR2"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); end; :: deftheorem defines :::"MULT210"::: GATE_5:def 1 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_gate_5 :::"MULT210"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ))); :: deftheorem defines :::"MULT211"::: GATE_5:def 2 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_gate_5 :::"MULT211"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT212"::: GATE_5:def 3 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_gate_5 :::"MULT212"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT213"::: GATE_5:def 4 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_gate_5 :::"MULT213"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k36_gate_1 :::"CARR2"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); theorem :: GATE_5:1 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "q00")) "," (Set (Var "q01")) "," (Set (Var "c01")) "," (Set (Var "q11")) "," (Set (Var "c11")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k1_gate_5 :::"MULT210"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_gate_5 :::"MULT210"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_5 :::"MULT211"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_5 :::"MULT211"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_5 :::"MULT212"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_gate_5 :::"MULT212"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k4_gate_5 :::"MULT213"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k4_gate_5 :::"MULT213"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; definitionlet "x0", "x1", "x2", "y0", "y1" be ($#m1_hidden :::"set"::: ) ; func :::"MULT310"::: "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 5 (Set ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y0" ")" ); func :::"MULT311"::: "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 6 (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT312"::: "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 7 (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT313"::: "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 8 (Set ($#k37_gate_1 :::"ADD3"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT314"::: "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 9 (Set ($#k38_gate_1 :::"CARR3"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y1" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y1" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); end; :: deftheorem defines :::"MULT310"::: GATE_5:def 5 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ))); :: deftheorem defines :::"MULT311"::: GATE_5:def 6 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT312"::: GATE_5:def 7 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_gate_5 :::"MULT312"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT313"::: GATE_5:def 8 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_gate_5 :::"MULT313"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k37_gate_1 :::"ADD3"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT314"::: GATE_5:def 9 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_gate_5 :::"MULT314"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k38_gate_1 :::"CARR3"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); definitionlet "x0", "x1", "x2", "y0", "y1", "y2" be ($#m1_hidden :::"set"::: ) ; func :::"MULT321"::: "(" "x2" "," "y2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 10 (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y2" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT322"::: "(" "x2" "," "y2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 11 (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set "(" ($#k8_gate_5 :::"MULT313"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y2" ")" ")" ) "," (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y2" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT323"::: "(" "x2" "," "y2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 12 (Set ($#k37_gate_1 :::"ADD3"::: ) "(" (Set "(" ($#k9_gate_5 :::"MULT314"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y2" ")" ")" ) "," (Set "(" ($#k8_gate_5 :::"MULT313"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y2" ")" ")" ) "," (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y2" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"MULT324"::: "(" "x2" "," "y2" "," "x1" "," "y1" "," "x0" "," "y0" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 13 (Set ($#k38_gate_1 :::"CARR3"::: ) "(" (Set "(" ($#k9_gate_5 :::"MULT314"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x2" "," "y2" ")" ")" ) "," (Set "(" ($#k8_gate_5 :::"MULT313"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x1" "," "y2" ")" ")" ) "," (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" "x2" "," "x1" "," "y1" "," "x0" "," "y0" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "x0" "," "y2" ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); end; :: deftheorem defines :::"MULT321"::: GATE_5:def 10 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT322"::: GATE_5:def 11 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set "(" ($#k8_gate_5 :::"MULT313"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT323"::: GATE_5:def 12 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k37_gate_1 :::"ADD3"::: ) "(" (Set "(" ($#k9_gate_5 :::"MULT314"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set "(" ($#k8_gate_5 :::"MULT313"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"MULT324"::: GATE_5:def 13 : (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k38_gate_1 :::"CARR3"::: ) "(" (Set "(" ($#k9_gate_5 :::"MULT314"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set "(" ($#k8_gate_5 :::"MULT313"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set "(" ($#k7_gate_5 :::"MULT312"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); theorem :: GATE_5:2 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "," (Set (Var "z5")) "," (Set (Var "q00")) "," (Set (Var "q01")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set (Var "c02")) "," (Set (Var "q11")) "," (Set (Var "q12")) "," (Set (Var "c11")) "," (Set (Var "c12")) "," (Set (Var "q21")) "," (Set (Var "q22")) "," (Set (Var "c21")) "," (Set (Var "c22")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q02")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q02")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c02")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c02")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q02")) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q02")) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q02")) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q02")) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c01")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c02")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c02")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c02")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c02")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q21")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q12")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q12")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q21")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c21")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q12")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q12")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c21")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q22")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c21")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c21")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q22")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c22")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c21")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c21")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c22")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q21")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q21")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q22")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q22")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c22")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c22")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; begin theorem :: GATE_5:3 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "," (Set (Var "z5")) "," (Set (Var "q00")) "," (Set (Var "q01")) "," (Set (Var "q02")) "," (Set (Var "q03")) "," (Set (Var "c01")) "," (Set (Var "c02")) "," (Set (Var "c03")) "," (Set (Var "q11")) "," (Set (Var "q12")) "," (Set (Var "q13")) "," (Set (Var "c11")) "," (Set (Var "c12")) "," (Set (Var "c13")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q02")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q02")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c02")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c02")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q03")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q03")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c03")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c03")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "c11")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "c12")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; notationlet "a1", "b1", "c" be ($#m1_hidden :::"set"::: ) ; synonym :::"CLAADD1"::: "(" "a1" "," "b1" "," "c" ")" for :::"XOR3"::: "(" "a1" "," "b1" "," "c" ")" ; synonym :::"CLACARR1"::: "(" "a1" "," "b1" "," "c" ")" for :::"MAJ3"::: "(" "a1" "," "b1" "," "c" ")" ; end; definitionlet "a1", "b1", "a2", "b2", "c" be ($#m1_hidden :::"set"::: ) ; func :::"CLAADD2"::: "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 14 (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a2" "," "b2" "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" "a1" "," "b1" "," "c" ")" ")" ) ")" ); func :::"CLACARR2"::: "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 15 (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "a2" "," "b2" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a2" "," "b2" ")" ")" ) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" "a1" "," "b1" "," "c" ")" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"CLAADD2"::: GATE_5:def 14 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_gate_5 :::"CLAADD2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); :: deftheorem defines :::"CLACARR2"::: GATE_5:def 15 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k15_gate_5 :::"CLACARR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ")" ) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "a3", "b3", "c" be ($#m1_hidden :::"set"::: ) ; func :::"CLAADD3"::: "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 16 (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a3" "," "b3" "," (Set "(" ($#k15_gate_5 :::"CLACARR2"::: ) "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" ")" ) ")" ); func :::"CLACARR3"::: "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 17 (Set ($#k9_gate_1 :::"OR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "a3" "," "b3" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a3" "," "b3" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "a2" "," "b2" ")" ")" ) ")" ")" ) "," (Set "(" ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a3" "," "b3" ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a2" "," "b2" ")" ")" ) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" "a1" "," "b1" "," "c" ")" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"CLAADD3"::: GATE_5:def 16 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k16_gate_5 :::"CLAADD3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set "(" ($#k15_gate_5 :::"CLACARR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); :: deftheorem defines :::"CLACARR3"::: GATE_5:def 17 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k17_gate_5 :::"CLACARR3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gate_1 :::"OR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ")" ) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "a3", "b3", "a4", "b4", "c" be ($#m1_hidden :::"set"::: ) ; func :::"CLAADD4"::: "(" "a4" "," "b4" "," "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 18 (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a4" "," "b4" "," (Set "(" ($#k17_gate_5 :::"CLACARR3"::: ) "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" ")" ) ")" ); func :::"CLACARR4"::: "(" "a4" "," "b4" "," "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_5:def 19 (Set ($#k15_gate_1 :::"OR4"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "a4" "," "b4" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a4" "," "b4" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "a3" "," "b3" ")" ")" ) ")" ")" ) "," (Set "(" ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a4" "," "b4" ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a3" "," "b3" ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" "a2" "," "b2" ")" ")" ) ")" ")" ) "," (Set "(" ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a4" "," "b4" ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a3" "," "b3" ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" "a2" "," "b2" ")" ")" ) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" "a1" "," "b1" "," "c" ")" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"CLAADD4"::: GATE_5:def 18 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a4")) "," (Set (Var "b4")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k18_gate_5 :::"CLAADD4"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) "," (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) "," (Set "(" ($#k17_gate_5 :::"CLACARR3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); :: deftheorem defines :::"CLACARR4"::: GATE_5:def 19 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a4")) "," (Set (Var "b4")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k19_gate_5 :::"CLACARR4"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) "," (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_gate_1 :::"OR4"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) ")" ")" ) "," (Set "(" ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ")" ) "," (Set "(" ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ")" ) ")" ))); theorem :: GATE_5:4 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "," (Set (Var "z5")) "," (Set (Var "q00")) "," (Set (Var "q01")) "," (Set (Var "q02")) "," (Set (Var "q03")) "," (Set (Var "c01")) "," (Set (Var "c02")) "," (Set (Var "c03")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y1")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q02")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q02")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c02")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y0")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x0")) "," (Set (Var "y2")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c02")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q03")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q03")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c03")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y2")) ")" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c03")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q00")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q01")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"CLAADD1"::: ) "(" (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"CLAADD1"::: ) "(" (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_5 :::"CLAADD2"::: ) "(" (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_5 :::"CLAADD2"::: ) "(" (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k16_gate_5 :::"CLAADD3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k16_gate_5 :::"CLAADD3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k17_gate_5 :::"CLACARR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k17_gate_5 :::"CLACARR3"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) "," (Set (Var "c03")) "," (Set (Var "q03")) "," (Set (Var "c02")) "," (Set (Var "q02")) "," (Set (Var "c01")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k5_gate_5 :::"MULT310"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_5 :::"MULT311"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_5 :::"MULT321"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_5 :::"MULT322"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k12_gate_5 :::"MULT323"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k13_gate_5 :::"MULT324"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x0")) "," (Set (Var "y0")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "z5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ;