:: GATE_2  semantic presentation begin  






theorem :: GATE_2:1 (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 "q1"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "q1"))) "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   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) "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   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q3")) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "q1")) ")" ) ")"  ")" ) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q1")) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q2")) "," (Set (Var "q3")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q3")) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "q1")) ")" ) ")"  ")" ) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q1")) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q2")) "," (Set (Var "q3")) ")"  ")" ) ")"  ")" ) ")" ) "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 "ns2")) "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 "ns2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "ns3")) "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 "ns3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "ns4")) "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 "ns4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "ns5")) "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 "ns5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "ns6")) "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 "ns6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "ns7")) "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 "ns7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "ns0")) "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 "ns0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"   ")" ))  ")" ))) ; 
 
theorem :: GATE_2:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Bool  "not" (Set   ($#k8_gate_1 :::"AND3"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "a")) "," (Set (Var "d")) ")"  ")" ) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "b")) "," (Set (Var "d")) ")"  ")" ) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) "iff" (Bool  "not" (Bool (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set  "("  ($#k8_gate_1 :::"AND3"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "d")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )) ; 
 
theorem :: GATE_2:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) "implies" (Bool  "not" (Bool (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "a")) ")" ) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "b")) ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "a")) ")" ) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "b")) ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "("  (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "d")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k8_gate_1 :::"AND3"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k8_gate_1 :::"AND3"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "("  (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "d")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )  ")"  & (Bool  "not" (Bool  "("  (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )) &  "("  (Bool (Bool (Bool  "not" (Set (Var "a")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  & (Bool (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" ))  ")" )) ; 
 
theorem :: GATE_2: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 "q1")) ")" ) "," (Set (Var "R")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "q1")) ")" ) "," (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  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q1")) "," (Set (Var "q2")) ")"  ")" ) "," (Set (Var "R")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q1")) "," (Set (Var "q2")) ")"  ")" ) "," (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  "("  ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q3")) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "q1")) ")" ) ")"  ")" ) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q1")) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q2")) "," (Set (Var "q3")) ")"  ")" ) ")"  ")" ) ")"  ")" ) "," (Set (Var "R")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set  "("  ($#k3_gate_1 :::"OR2"::: )   "(" (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q3")) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "q1")) ")" ) ")"  ")" ) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "q1")) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "q2")) "," (Set (Var "q3")) ")"  ")" ) ")"  ")" ) ")"  ")" ) "," (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 "ns2")) "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 "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 "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 "ns3")) "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 "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 "ns4")) "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 "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 "ns5")) "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 "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 "ns6")) "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 "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 "ns7")) "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 (Var "s7")) "," (Set  "("  ($#k1_gate_1 :::"NOT1"::: )  (Set (Var "R")) ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k3_gate_1 :::"OR2"::: )   "(" (Set (Var "s7")) "," (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"::: )  ))  ")"   ")" ))  ")" ))) ;