:: GATE_1 semantic presentation begin definitionlet "a" be ($#m1_hidden :::"set"::: ) ; func :::"NOT1"::: "a" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 1 (Set ($#k1_xboole_0 :::"{}"::: ) ) if (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) otherwise (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ); end; :: deftheorem defines :::"NOT1"::: GATE_1:def 1 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ")" )); registrationlet "a" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_gate_1 :::"NOT1"::: ) "a") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_gate_1 :::"NOT1"::: ) "a") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:1 (Bool "(" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ) ; theorem :: GATE_1:2 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "a"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; theorem :: GATE_1:3 (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"AND2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 2 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; end; :: deftheorem defines :::"AND2"::: GATE_1:def 2 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); registrationlet "a", "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_gate_1 :::"AND2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_gate_1 :::"AND2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"OR2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 3 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; end; :: deftheorem defines :::"OR2"::: GATE_1:def 3 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); registrationlet "a" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_gate_1 :::"OR2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_gate_1 :::"OR2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"XOR2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 4 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; end; :: deftheorem defines :::"XOR2"::: GATE_1:def 4 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); registrationlet "a" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_gate_1 :::"XOR2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_gate_1 :::"XOR2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "a", "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_gate_1 :::"XOR2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) "iff" (Bool "not" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; theorem :: GATE_1:7 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; theorem :: GATE_1:8 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; theorem :: GATE_1:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "not" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"EQV2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 5 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool (Bool "not" (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ")" )) & "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool (Bool "not" (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ")" )) & "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; end; :: deftheorem defines :::"EQV2"::: GATE_1:def 5 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool (Bool "not" (Set ($#k5_gate_1 :::"EQV2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ")" )) & "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) "implies" (Bool (Set ($#k5_gate_1 :::"EQV2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); registrationlet "a" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_gate_1 :::"EQV2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "a", "b" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_gate_1 :::"EQV2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_gate_1 :::"EQV2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GATE_1:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k5_gate_1 :::"EQV2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; theorem :: GATE_1:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k5_gate_1 :::"EQV2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"NAND2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 6 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; end; :: deftheorem defines :::"NAND2"::: GATE_1:def 6 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); registrationlet "a" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_gate_1 :::"NAND2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_gate_1 :::"NAND2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"NOR2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 7 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; end; :: deftheorem defines :::"NOR2"::: GATE_1:def 7 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); registrationlet "a", "b" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_gate_1 :::"NOR2"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_gate_1 :::"NOR2"::: ) "(" "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func :::"AND3"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 8 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"AND3"::: GATE_1:def 8 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); registrationlet "a", "b", "c" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_gate_1 :::"AND3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "b", "c" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_gate_1 :::"AND3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k8_gate_1 :::"AND3"::: ) "(" "b" "," "a" "," "c" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k8_gate_1 :::"AND3"::: ) "(" "b" "," "c" "," "a" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func :::"OR3"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 9 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"OR3"::: GATE_1:def 9 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k9_gate_1 :::"OR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k9_gate_1 :::"OR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); registrationlet "a", "b", "c" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_gate_1 :::"OR3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "a" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b", "c" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_gate_1 :::"OR3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k9_gate_1 :::"OR3"::: ) "(" "b" "," "a" "," "c" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k9_gate_1 :::"OR3"::: ) "(" "b" "," "c" "," "a" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GATE_1:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k9_gate_1 :::"OR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func :::"XOR3"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 10 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "(" (Bool "(" (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool "not" (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"XOR3"::: GATE_1:def 10 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool "(" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool "not" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" (Bool "(" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool "not" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); registrationlet "a", "b", "c" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "a", "b" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "c" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a" "," "c" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "c" "," "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "c" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a" "," "c" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "c" "," "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "a", "b", "c" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GATE_1:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool "(" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool "not" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) "iff" (Bool "not" (Bool (Set ($#k10_gate_1 :::"XOR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func :::"MAJ3"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 11 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"MAJ3"::: GATE_1:def 11 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); registrationlet "a", "b" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "c" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a" "," "c" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "c" "," "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "c" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a" "," "c" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "c" "," "a" "," "b" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: GATE_1:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ) "iff" (Bool "not" (Bool (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func :::"NAND3"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 12 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NAND3"::: GATE_1:def 12 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k12_gate_1 :::"NAND3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k12_gate_1 :::"NAND3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k12_gate_1 :::"NAND3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func :::"NOR3"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 13 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NOR3"::: GATE_1:def 13 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k13_gate_1 :::"NOR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k13_gate_1 :::"NOR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k13_gate_1 :::"NOR3"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; definitionlet "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; func :::"AND4"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 14 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "d" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"AND4"::: GATE_1:def 14 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; func :::"OR4"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 15 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"OR4"::: GATE_1:def 15 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k15_gate_1 :::"OR4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k15_gate_1 :::"OR4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); theorem :: GATE_1:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k15_gate_1 :::"OR4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; func :::"NAND4"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 16 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NAND4"::: GATE_1:def 16 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k16_gate_1 :::"NAND4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k16_gate_1 :::"NAND4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k16_gate_1 :::"NAND4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; func :::"NOR4"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 17 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NOR4"::: GATE_1:def 17 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k17_gate_1 :::"NOR4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k17_gate_1 :::"NOR4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k17_gate_1 :::"NOR4"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e" be ($#m1_hidden :::"set"::: ) ; func :::"AND5"::: "(" "a" "," "b" "," "c" "," "d" "," "e" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 18 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "d" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "e" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"AND5"::: GATE_1:def 18 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k18_gate_1 :::"AND5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k18_gate_1 :::"AND5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:24 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k18_gate_1 :::"AND5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e" be ($#m1_hidden :::"set"::: ) ; func :::"OR5"::: "(" "a" "," "b" "," "c" "," "d" "," "e" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 19 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"OR5"::: GATE_1:def 19 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k19_gate_1 :::"OR5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k19_gate_1 :::"OR5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); theorem :: GATE_1:25 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k19_gate_1 :::"OR5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c", "d", "e" be ($#m1_hidden :::"set"::: ) ; func :::"NAND5"::: "(" "a" "," "b" "," "c" "," "d" "," "e" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 20 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NAND5"::: GATE_1:def 20 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k20_gate_1 :::"NAND5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k20_gate_1 :::"NAND5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:26 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k20_gate_1 :::"NAND5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b", "c", "d", "e" be ($#m1_hidden :::"set"::: ) ; func :::"NOR5"::: "(" "a" "," "b" "," "c" "," "d" "," "e" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 21 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NOR5"::: GATE_1:def 21 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k21_gate_1 :::"NOR5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k21_gate_1 :::"NOR5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:27 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k21_gate_1 :::"NOR5"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f" be ($#m1_hidden :::"set"::: ) ; func :::"AND6"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 22 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "d" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "e" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "f" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"AND6"::: GATE_1:def 22 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k22_gate_1 :::"AND6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k22_gate_1 :::"AND6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:28 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k22_gate_1 :::"AND6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f" be ($#m1_hidden :::"set"::: ) ; func :::"OR6"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 23 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"OR6"::: GATE_1:def 23 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k23_gate_1 :::"OR6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k23_gate_1 :::"OR6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); theorem :: GATE_1:29 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k23_gate_1 :::"OR6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f" be ($#m1_hidden :::"set"::: ) ; func :::"NAND6"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 24 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NAND6"::: GATE_1:def 24 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k24_gate_1 :::"NAND6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k24_gate_1 :::"NAND6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:30 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k24_gate_1 :::"NAND6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f" be ($#m1_hidden :::"set"::: ) ; func :::"NOR6"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 25 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NOR6"::: GATE_1:def 25 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k25_gate_1 :::"NOR6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k25_gate_1 :::"NOR6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:31 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k25_gate_1 :::"NOR6"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g" be ($#m1_hidden :::"set"::: ) ; func :::"AND7"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 26 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "d" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "e" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "f" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "g" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"AND7"::: GATE_1:def 26 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k26_gate_1 :::"AND7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k26_gate_1 :::"AND7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:32 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k26_gate_1 :::"AND7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g" be ($#m1_hidden :::"set"::: ) ; func :::"OR7"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 27 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "g" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"OR7"::: GATE_1:def 27 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k27_gate_1 :::"OR7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k27_gate_1 :::"OR7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); theorem :: GATE_1:33 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k27_gate_1 :::"OR7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g" be ($#m1_hidden :::"set"::: ) ; func :::"NAND7"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 28 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "g" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NAND7"::: GATE_1:def 28 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k28_gate_1 :::"NAND7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k28_gate_1 :::"NAND7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:34 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k28_gate_1 :::"NAND7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g" be ($#m1_hidden :::"set"::: ) ; func :::"NOR7"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 29 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "g" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NOR7"::: GATE_1:def 29 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k29_gate_1 :::"NOR7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k29_gate_1 :::"NOR7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:35 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k29_gate_1 :::"NOR7"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g", "h" be ($#m1_hidden :::"set"::: ) ; func :::"AND8"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" "," "h" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 30 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool (Bool "not" "a" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "b" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "c" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "d" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "e" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "f" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "g" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" "h" "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"AND8"::: GATE_1:def 30 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k30_gate_1 :::"AND8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k30_gate_1 :::"AND8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:36 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k30_gate_1 :::"AND8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g", "h" be ($#m1_hidden :::"set"::: ) ; func :::"OR8"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" "," "h" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 31 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "g" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "h" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"OR8"::: GATE_1:def 31 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k31_gate_1 :::"OR8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k31_gate_1 :::"OR8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); theorem :: GATE_1:37 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "iff" (Bool "not" (Bool (Set ($#k31_gate_1 :::"OR8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g", "h" be ($#m1_hidden :::"set"::: ) ; func :::"NAND8"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" "," "h" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 32 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "g" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "h" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NAND8"::: GATE_1:def 32 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k32_gate_1 :::"NAND8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k32_gate_1 :::"NAND8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:38 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k32_gate_1 :::"NAND8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; definitionlet "a", "b", "c", "d", "e", "f", "g", "h" be ($#m1_hidden :::"set"::: ) ; func :::"NOR8"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "g" "," "h" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 33 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "c" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "d" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "e" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "f" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "g" "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool "h" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"NOR8"::: GATE_1:def 33 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k33_gate_1 :::"NOR8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k33_gate_1 :::"NOR8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:39 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k33_gate_1 :::"NOR8"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "c")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "e")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" )) ; begin theorem :: GATE_1:40 (Bool "for" (Set (Var "c1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "," (Set (Var "c2")) "," (Set (Var "c3")) "," (Set (Var "c4")) "," (Set (Var "c5")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n")) "," (Set (Var "c5b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "c2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "c3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) "," (Set (Var "c4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k18_gate_1 :::"AND5"::: ) "(" (Set (Var "c1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c5b")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "c5")) "," (Set (Var "n")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set (Var "c5")) "," (Set (Var "n")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c5b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "c5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "not" (Bool (Set (Var "c5b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"MODADD2"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 34 (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool "(" (Bool "(" "not" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) & (Bool "(" (Bool "a" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "b" "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; end; :: deftheorem defines :::"MODADD2"::: GATE_1:def 34 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_gate_1 :::"NOT1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" & "(" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "implies" (Bool (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: GATE_1:41 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool "(" (Bool "(" "not" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ) ")" )) ; notationlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; synonym :::"ADD1"::: "(" "a" "," "b" "," "c" ")" for :::"XOR3"::: "(" "a" "," "b" "," "c" ")" ; synonym :::"CARR1"::: "(" "a" "," "b" "," "c" ")" for :::"MAJ3"::: "(" "a" "," "b" "," "c" ")" ; end; definitionlet "a1", "b1", "a2", "b2", "c" be ($#m1_hidden :::"set"::: ) ; func :::"ADD2"::: "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 35 (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a2" "," "b2" "," (Set "(" ($#k11_gate_1 :::"CARR1"::: ) "(" "a1" "," "b1" "," "c" ")" ")" ) ")" ); end; :: deftheorem defines :::"ADD2"::: GATE_1:def 35 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (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 :::"CARR1"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "c" be ($#m1_hidden :::"set"::: ) ; func :::"CARR2"::: "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 36 (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a2" "," "b2" "," (Set "(" ($#k11_gate_1 :::"CARR1"::: ) "(" "a1" "," "b1" "," "c" ")" ")" ) ")" ); end; :: deftheorem defines :::"CARR2"::: GATE_1:def 36 : (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k36_gate_1 :::"CARR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set "(" ($#k11_gate_1 :::"CARR1"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "a3", "b3", "c" be ($#m1_hidden :::"set"::: ) ; func :::"ADD3"::: "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 37 (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a3" "," "b3" "," (Set "(" ($#k36_gate_1 :::"CARR2"::: ) "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" ")" ) ")" ); end; :: deftheorem defines :::"ADD3"::: GATE_1:def 37 : (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 ($#k37_gate_1 :::"ADD3"::: ) "(" (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 "(" ($#k36_gate_1 :::"CARR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "a3", "b3", "c" be ($#m1_hidden :::"set"::: ) ; func :::"CARR3"::: "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 38 (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a3" "," "b3" "," (Set "(" ($#k36_gate_1 :::"CARR2"::: ) "(" "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" ")" ) ")" ); end; :: deftheorem defines :::"CARR3"::: GATE_1:def 38 : (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 ($#k38_gate_1 :::"CARR3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set "(" ($#k36_gate_1 :::"CARR2"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "a3", "b3", "a4", "b4", "c" be ($#m1_hidden :::"set"::: ) ; func :::"ADD4"::: "(" "a4" "," "b4" "," "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 39 (Set ($#k10_gate_1 :::"XOR3"::: ) "(" "a4" "," "b4" "," (Set "(" ($#k38_gate_1 :::"CARR3"::: ) "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" ")" ) ")" ); end; :: deftheorem defines :::"ADD4"::: GATE_1:def 39 : (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 ($#k39_gate_1 :::"ADD4"::: ) "(" (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 "(" ($#k38_gate_1 :::"CARR3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); definitionlet "a1", "b1", "a2", "b2", "a3", "b3", "a4", "b4", "c" be ($#m1_hidden :::"set"::: ) ; func :::"CARR4"::: "(" "a4" "," "b4" "," "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: GATE_1:def 40 (Set ($#k11_gate_1 :::"MAJ3"::: ) "(" "a4" "," "b4" "," (Set "(" ($#k38_gate_1 :::"CARR3"::: ) "(" "a3" "," "b3" "," "a2" "," "b2" "," "a1" "," "b1" "," "c" ")" ")" ) ")" ); end; :: deftheorem defines :::"CARR4"::: GATE_1:def 40 : (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 ($#k40_gate_1 :::"CARR4"::: ) "(" (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 ($#k11_gate_1 :::"MAJ3"::: ) "(" (Set (Var "a4")) "," (Set (Var "b4")) "," (Set "(" ($#k38_gate_1 :::"CARR3"::: ) "(" (Set (Var "a3")) "," (Set (Var "b3")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c")) ")" ")" ) ")" ))); theorem :: GATE_1:42 (Bool "for" (Set (Var "c1")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x4")) "," (Set (Var "y4")) "," (Set (Var "c4")) "," (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "sd1")) "," (Set (Var "q2")) "," (Set (Var "p2")) "," (Set (Var "sd2")) "," (Set (Var "q3")) "," (Set (Var "p3")) "," (Set (Var "sd3")) "," (Set (Var "q4")) "," (Set (Var "p4")) "," (Set (Var "sd4")) "," (Set (Var "cb1")) "," (Set (Var "cb2")) "," (Set (Var "l2")) "," (Set (Var "t2")) "," (Set (Var "l3")) "," (Set (Var "m3")) "," (Set (Var "t3")) "," (Set (Var "l4")) "," (Set (Var "m4")) "," (Set (Var "n4")) "," (Set (Var "t4")) "," (Set (Var "l5")) "," (Set (Var "m5")) "," (Set (Var "n5")) "," (Set (Var "o5")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "s4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "p1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "sd1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "sd1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "p2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "sd2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "sd2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "p3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "sd3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "sd3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_gate_1 :::"NAND2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "p4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "sd4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k34_gate_1 :::"MODADD2"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "sd4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "cb1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "c1"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "c1"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "cb1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "cb2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "cb1"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "cb1"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "cb2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "cb2")) "," (Set (Var "sd1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "cb2")) "," (Set (Var "sd1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "l2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "cb1")) "," (Set (Var "p1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "cb1")) "," (Set (Var "p1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "l2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "t2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "l2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k7_gate_1 :::"NOR2"::: ) "(" (Set (Var "l2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "t2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "t2")) "," (Set (Var "sd2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "t2")) "," (Set (Var "sd2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "l3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "p2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "p2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "l3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "m3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "cb1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "cb1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "m3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "t3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k13_gate_1 :::"NOR3"::: ) "(" (Set (Var "l3")) "," (Set (Var "m3")) "," (Set (Var "q2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k13_gate_1 :::"NOR3"::: ) "(" (Set (Var "l3")) "," (Set (Var "m3")) "," (Set (Var "q2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "t3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "t3")) "," (Set (Var "sd3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "t3")) "," (Set (Var "sd3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "l4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "p3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "p3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "l4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "m4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "m4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "cb1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "cb1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "n4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "t4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k17_gate_1 :::"NOR4"::: ) "(" (Set (Var "l4")) "," (Set (Var "m4")) "," (Set (Var "n4")) "," (Set (Var "q3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k17_gate_1 :::"NOR4"::: ) "(" (Set (Var "l4")) "," (Set (Var "m4")) "," (Set (Var "n4")) "," (Set (Var "q3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "t4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "t4")) "," (Set (Var "sd4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k4_gate_1 :::"XOR2"::: ) "(" (Set (Var "t4")) "," (Set (Var "sd4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "l5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q3")) "," (Set (Var "p4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q3")) "," (Set (Var "p4")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "l5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "m5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q2")) "," (Set (Var "p4")) "," (Set (Var "p3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q2")) "," (Set (Var "p4")) "," (Set (Var "p3")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "m5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q1")) "," (Set (Var "p4")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q1")) "," (Set (Var "p4")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "n5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "o5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k18_gate_1 :::"AND5"::: ) "(" (Set (Var "p4")) "," (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "cb1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k18_gate_1 :::"AND5"::: ) "(" (Set (Var "p4")) "," (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "cb1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "o5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k21_gate_1 :::"NOR5"::: ) "(" (Set (Var "q4")) "," (Set (Var "l5")) "," (Set (Var "m5")) "," (Set (Var "n5")) "," (Set (Var "o5")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k21_gate_1 :::"NOR5"::: ) "(" (Set (Var "q4")) "," (Set (Var "l5")) "," (Set (Var "m5")) "," (Set (Var "n5")) "," (Set (Var "o5")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k10_gate_1 :::"ADD1"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k35_gate_1 :::"ADD2"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k37_gate_1 :::"ADD3"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k37_gate_1 :::"ADD3"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k39_gate_1 :::"ADD4"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) "," (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k39_gate_1 :::"ADD4"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) "," (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k40_gate_1 :::"CARR4"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) "," (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k40_gate_1 :::"CARR4"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) "," (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "c1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "c4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ;