:: GATE_3 semantic presentation begin theorem :: GATE_3:1 (Bool "for" (Set (Var "s0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "ns0")) "," (Set (Var "ns1")) "," (Set (Var "ns2")) "," (Set (Var "ns3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "nq1")) "," (Set (Var "nq2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "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 ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "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 ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; theorem :: GATE_3:2 (Bool "for" (Set (Var "s0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "ns0")) "," (Set (Var "ns1")) "," (Set (Var "ns2")) "," (Set (Var "ns3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "nq1")) "," (Set (Var "nq2")) "," (Set (Var "R")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "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 ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "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 ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s0")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s0")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s2")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s2")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; theorem :: GATE_3:3 (Bool "for" (Set (Var "s0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "s4")) "," (Set (Var "s5")) "," (Set (Var "s6")) "," (Set (Var "s7")) "," (Set (Var "ns0")) "," (Set (Var "ns1")) "," (Set (Var "ns2")) "," (Set (Var "ns3")) "," (Set (Var "ns4")) "," (Set (Var "ns5")) "," (Set (Var "ns6")) "," (Set (Var "ns7")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "nq1")) "," (Set (Var "nq2")) "," (Set (Var "nq3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "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 ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "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 ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "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 ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; theorem :: GATE_3:4 (Bool "for" (Set (Var "s0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "s4")) "," (Set (Var "s5")) "," (Set (Var "s6")) "," (Set (Var "s7")) "," (Set (Var "ns0")) "," (Set (Var "ns1")) "," (Set (Var "ns2")) "," (Set (Var "ns3")) "," (Set (Var "ns4")) "," (Set (Var "ns5")) "," (Set (Var "ns6")) "," (Set (Var "ns7")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "nq1")) "," (Set (Var "nq2")) "," (Set (Var "nq3")) "," (Set (Var "R")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "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 ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "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 ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "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 ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k8_gate_1 :::"AND3"::: ) "(" (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s0")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s0")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s7")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s7")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s6")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s6")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s4")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s4")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s5")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s5")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; theorem :: GATE_3:5 (Bool "for" (Set (Var "s0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "s4")) "," (Set (Var "s5")) "," (Set (Var "s6")) "," (Set (Var "s7")) "," (Set (Var "s8")) "," (Set (Var "s9")) "," (Set (Var "s10")) "," (Set (Var "s11")) "," (Set (Var "s12")) "," (Set (Var "s13")) "," (Set (Var "s14")) "," (Set (Var "s15")) "," (Set (Var "ns0")) "," (Set (Var "ns1")) "," (Set (Var "ns2")) "," (Set (Var "ns3")) "," (Set (Var "ns4")) "," (Set (Var "ns5")) "," (Set (Var "ns6")) "," (Set (Var "ns7")) "," (Set (Var "ns8")) "," (Set (Var "ns9")) "," (Set (Var "ns10")) "," (Set (Var "ns11")) "," (Set (Var "ns12")) "," (Set (Var "ns13")) "," (Set (Var "ns14")) "," (Set (Var "ns15")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "nq1")) "," (Set (Var "nq2")) "," (Set (Var "nq3")) "," (Set (Var "nq4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "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 ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "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 ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "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 ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "q3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ; theorem :: GATE_3:6 (Bool "for" (Set (Var "s0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "s4")) "," (Set (Var "s5")) "," (Set (Var "s6")) "," (Set (Var "s7")) "," (Set (Var "s8")) "," (Set (Var "s9")) "," (Set (Var "s10")) "," (Set (Var "s11")) "," (Set (Var "s12")) "," (Set (Var "s13")) "," (Set (Var "s14")) "," (Set (Var "s15")) "," (Set (Var "ns0")) "," (Set (Var "ns1")) "," (Set (Var "ns2")) "," (Set (Var "ns3")) "," (Set (Var "ns4")) "," (Set (Var "ns5")) "," (Set (Var "ns6")) "," (Set (Var "ns7")) "," (Set (Var "ns8")) "," (Set (Var "ns9")) "," (Set (Var "ns10")) "," (Set (Var "ns11")) "," (Set (Var "ns12")) "," (Set (Var "ns13")) "," (Set (Var "ns14")) "," (Set (Var "ns15")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "nq1")) "," (Set (Var "nq2")) "," (Set (Var "nq3")) "," (Set (Var "nq4")) "," (Set (Var "R")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "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 ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "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 ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "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 ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q3")) ")" ) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q2")) ")" ) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "q4")) "," (Set (Var "q3")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "s15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq4")) ")" ) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq3")) ")" ) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq2")) ")" ) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "nq1")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k14_gate_1 :::"AND4"::: ) "(" (Set (Var "nq4")) "," (Set (Var "nq3")) "," (Set (Var "nq2")) "," (Set (Var "nq1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "q4")) ")" ) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "nq4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "q3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "nq4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & (Bool "not" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s0")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s0")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s1")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns3")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s3")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns7")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s7")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s7")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns15")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s15")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s15")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns14")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s14")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s14")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns12")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s12")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s12")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns8")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s8")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_gate_1 :::"OR2"::: ) "(" (Set "(" ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s8")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k1_gate_1 :::"NOT1"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns0")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s2")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns5")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s5")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s5")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns11")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s11")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s11")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns6")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s6")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s6")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns13")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s13")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s13")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns10")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s10")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s10")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns4")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s4")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s4")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns9")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s9")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_gate_1 :::"AND2"::: ) "(" (Set (Var "s9")) "," (Set (Var "R")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "ns2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )) ")" ))) ;