:: CIRCCMB3 semantic presentation begin theorem :: CIRCCMB3:1 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "A")); attr "s" is :::"stabilizing"::: means :: CIRCCMB3:def 1 (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" "s" "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )); end; :: deftheorem defines :::"stabilizing"::: CIRCCMB3:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) ")" )))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S")); attr "A" is :::"stabilizing"::: means :: CIRCCMB3:def 2 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" "A" "holds" (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )); attr "A" is :::"with_stabilization-limit"::: means :: CIRCCMB3:def 3 (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" "A" "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))); end; :: deftheorem defines :::"stabilizing"::: CIRCCMB3:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_circcmb3 :::"stabilizing"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) ")" ))); :: deftheorem defines :::"with_stabilization-limit"::: CIRCCMB3:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_circcmb3 :::"with_stabilization-limit"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))) ")" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#v3_circcmb3 :::"with_stabilization-limit"::: ) -> ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_circcmb3 :::"stabilizing"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "A")); assume (Bool (Set (Const "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ) ; func :::"Result"::: "s" -> ($#m1_subset_1 :::"State":::) "of" "A" means :: CIRCCMB3:def 4 (Bool "(" (Bool it "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool it ($#r8_pboole :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" "s" "," (Set (Var "n")) ")" ))) ")" ); end; :: deftheorem defines :::"Result"::: CIRCCMB3:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set (Var "b4")) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "b4")) ($#r8_pboole :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ))) ")" ) ")" ))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "A")); assume (Bool (Set (Const "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ) ; func :::"stabilization-time"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: CIRCCMB3:def 5 (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" "s" "," it ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) it)) "holds" (Bool "not" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" "s" "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"stabilization-time"::: CIRCCMB3:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "b4")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b4")))) "holds" (Bool "not" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) ")" ) ")" ) ")" ))))); theorem :: CIRCCMB3:2 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool (Set ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s"))) ($#r8_pboole :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s")) ")" ) ")" ))))) ; theorem :: CIRCCMB3:3 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))))))) ; theorem :: CIRCCMB3:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s"))) ($#r8_pboole :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" )))))) ; theorem :: CIRCCMB3:5 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s"))) ($#r8_pboole :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" )))))) ; theorem :: CIRCCMB3:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: CIRCCMB3:7 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ) & (Bool (Set (Var "s2")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ))))))))) ; theorem :: CIRCCMB3:8 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s2")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s1")) ")" ) "," (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s2")) ")" ) ")" )))))))))) ; theorem :: CIRCCMB3:9 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s1")) ")" ) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s2")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool (Set (Var "s")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) ))))))))) ; theorem :: CIRCCMB3:10 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s1")) ")" ) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s2")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s2")) ")" ))))))))))) ; theorem :: CIRCCMB3:11 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s1")) ")" ) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s2")) "is" ($#v1_circcmb3 :::"stabilizing"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) ($#r1_hidden :::"="::: ) (Set ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s1"))))))))))) ; begin theorem :: CIRCCMB3:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "g")) ")" ")" ) "holds" (Bool (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p"))) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))))))))) ; theorem :: CIRCCMB3:13 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k7_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: CIRCCMB3:14 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k8_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k8_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ))) ; definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "S" is :::"one-gate"::: means :: CIRCCMB3:def 6 (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) "st" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )))))); end; :: deftheorem defines :::"one-gate"::: CIRCCMB3:def 6 : (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_circcmb3 :::"one-gate"::: ) ) "iff" (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )))))) ")" )); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "A" is :::"one-gate"::: means :: CIRCCMB3:def 7 (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) "st" (Bool "(" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) ")" ))))); end; :: deftheorem defines :::"one-gate"::: CIRCCMB3:def 7 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_circcmb3 :::"one-gate"::: ) ) "iff" (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) ")" ))))) ")" ))); registrationlet "p" be ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "x" ")" ) -> ($#v8_struct_0 :::"finite"::: ) ; end; registration cluster ($#v4_circcmb3 :::"one-gate"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_circcmb3 :::"one-gate"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_circcomb :::"gate`2=den"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) -> ($#v4_circcmb3 :::"one-gate"::: ) ; end; registration cluster ($#v4_circcmb3 :::"one-gate"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registrationlet "S" be ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msafree2 :::"finite-yielding"::: ) ($#v5_circcmb3 :::"one-gate"::: ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" "p" "," "f" ")" ) -> ($#v5_circcmb3 :::"one-gate"::: ) ; end; registrationlet "S" be ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#v5_circcmb3 :::"one-gate"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; definitionlet "S" be ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"Output"::: "S" -> ($#m1_subset_1 :::"Vertex":::) "of" "S" equals :: CIRCCMB3:def 8 (Set ($#k3_tarski :::"union"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S")); end; :: deftheorem defines :::"Output"::: CIRCCMB3:def 8 : (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))))); registrationlet "S" be ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k3_circcmb3 :::"Output"::: ) "S") -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: CIRCCMB3:15 (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ))) "holds" (Bool (Set ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: CIRCCMB3:16 (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: CIRCCMB3:17 (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ))) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )))))))) ; theorem :: CIRCCMB3:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: CIRCCMB3:19 (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#v5_circcmb3 :::"one-gate"::: ) -> ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_circcmb3 :::"with_stabilization-limit"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; theorem :: CIRCCMB3:20 (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s"))) ($#r8_pboole :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))))))) ; theorem :: CIRCCMB3:21 (Bool "for" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1))))) ; scheme :: CIRCCMB3:sch 1 OneGate1Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set F1 "(" ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ) ")" ) ")" )) ")" ) ")" ))) proof end; scheme :: CIRCCMB3:sch 2 OneGate2Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ) ")" ) ")" )) ")" ) ")" ))) proof end; scheme :: CIRCCMB3:sch 3 OneGate3Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) } : (Bool "ex" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k1_enumset1 :::"}"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ) ")" ) ")" )) ")" ) ")" ))) proof end; scheme :: CIRCCMB3:sch 4 OneGate4Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ) } : (Bool "ex" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k2_enumset1 :::"}"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) ")" )) ")" ) ")" ))) proof end; scheme :: CIRCCMB3:sch 5 OneGate5Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"set"::: ) , F6() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ) } : (Bool "ex" (Set (Var "S")) "being" ($#v4_circcmb3 :::"one-gate"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v5_circcmb3 :::"one-gate"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) ($#k3_enumset1 :::"}"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) ")" )) ")" ) ")" ))) proof end; begin theorem :: CIRCCMB3:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ))) ; theorem :: CIRCCMB3:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Var "v")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )))) ; theorem :: CIRCCMB3:24 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S2")) "holds" (Bool (Set (Var "v")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; mode :::"Signature"::: "of" "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: CIRCCMB3:def 9 (Bool "ex" (Set (Var "A")) "being" ($#l3_msualg_1 :::"Circuit":::) "of" it "st" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) ($#r1_hidden :::"="::: ) "X") & (Bool (Set (Var "A")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) ")" )); end; :: deftheorem defines :::"Signature"::: CIRCCMB3:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "b2")) "st" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "A")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) ")" )) ")" ))); theorem :: CIRCCMB3:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X"))))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msualg_1 :::"strict"::: ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#v4_circcmb3 :::"one-gate"::: ) for ($#m1_circcmb3 :::"Signature"::: ) "of" "X"; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); :: original: :::"1GateCircStr"::: redefine func :::"1GateCircStr"::: "(" "p" "," "f" ")" -> ($#v1_msualg_1 :::"strict"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" "X"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); mode :::"Circuit"::: "of" "X" "," "S" -> ($#l3_msualg_1 :::"Circuit":::) "of" "S" means :: CIRCCMB3:def 10 (Bool "(" (Bool it "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it)) ($#r1_hidden :::"="::: ) "X") ")" ); end; :: deftheorem defines :::"Circuit"::: CIRCCMB3:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S"))) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b3"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b3")))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); cluster -> ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) for ($#m2_circcmb3 :::"Circuit"::: ) "of" "X" "," "S"; end; theorem :: CIRCCMB3:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v4_circcmb3 :::"one-gate"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v5_circcmb3 :::"one-gate"::: ) for ($#m2_circcmb3 :::"Circuit"::: ) "of" "X" "," "S"; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#v4_circcomb :::"gate`2=den"::: ) for ($#m2_circcmb3 :::"Circuit"::: ) "of" "X" "," "S"; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); :: original: :::"1GateCircuit"::: redefine func :::"1GateCircuit"::: "(" "p" "," "f" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#m2_circcmb3 :::"Circuit"::: ) "of" "X" "," (Set ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ); end; theorem :: CIRCCMB3:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S2")) "holds" (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))))))) ; theorem :: CIRCCMB3:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S2")) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) "is" ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")))))))) ; theorem :: CIRCCMB3:29 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S2")) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) "is" ($#v4_circcomb :::"gate`2=den"::: ) ))))) ; theorem :: CIRCCMB3:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S2")) "holds" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" )) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))))) ; registrationlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#v8_struct_0 :::"finite"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S1", "S2" be ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#v5_circcomb :::"gate`2=den"::: ) ; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S1", "S2" be ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); :: original: :::"+*"::: redefine func "S1" :::"+*"::: "S2" -> ($#v1_msualg_1 :::"strict"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" "X"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S1", "S2" be ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "A1" be ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Const "X")) "," (Set (Const "S1")); let "A2" be ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Const "X")) "," (Set (Const "S2")); :: original: :::"+*"::: redefine func "A1" :::"+*"::: "A2" -> ($#v3_msualg_1 :::"strict"::: ) ($#m2_circcmb3 :::"Circuit"::: ) "of" "X" "," (Set "S1" ($#k6_circcmb3 :::"+*"::: ) "S2"); end; theorem :: CIRCCMB3:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) ")" )) ; theorem :: CIRCCMB3:32 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_circcomb :::"gate`2=den"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v3_circcmb3 :::"with_stabilization-limit"::: ) ))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); cluster -> ($#v3_circcmb3 :::"with_stabilization-limit"::: ) for ($#m2_circcmb3 :::"Circuit"::: ) "of" "X" "," "S"; end; scheme :: CIRCCMB3:sch 6 1AryDef{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )))) & (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" ) proof end; scheme :: CIRCCMB3:sch 7 2AryDef{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) & (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" ) proof end; scheme :: CIRCCMB3:sch 8 3AryDef{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )))) & (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" ) proof end; theorem :: CIRCCMB3:33 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k7_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x4")) ")" ) ($#k7_finseq_4 :::"*>"::: ) )))) ; theorem :: CIRCCMB3:34 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x5")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k8_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k8_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x4")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x5")) ")" ) ($#k8_finseq_4 :::"*>"::: ) )))) ; scheme :: CIRCCMB3:sch 9 OneGate1Result{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F2 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set F4 "(" ")" ) ")" ")" ) (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set F4 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "a1")) ")" )))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F2 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F4 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a1")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "a1")) ")" ))) ")" )) proof end; scheme :: CIRCCMB3:sch 10 OneGate2Result{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F3 "(" ")" ) ")" ) "," (Set F3 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set F5 "(" ")" ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set F5 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" )))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F3 "(" ")" ) ")" ) "," (Set F3 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F5 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" ))) ")" )) proof end; scheme :: CIRCCMB3:sch 11 OneGate3Result{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ), F6() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F4 "(" ")" ) ")" ) "," (Set F4 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set F6 "(" ")" ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set F6 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F4 "(" ")" ) ")" ) "," (Set F4 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F6 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" ))) ")" )) proof end; scheme :: CIRCCMB3:sch 12 OneGate4Result{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ), F7() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 4) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F5 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k7_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k7_finseq_4 :::"*>"::: ) ) "," (Set F7 "(" ")" ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k7_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k7_finseq_4 :::"*>"::: ) ) "," (Set F7 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ")" )))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 4) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F5 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F7 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k9_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ($#k9_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ")" ))) ")" )) proof end; scheme :: CIRCCMB3:sch 13 OneGate5Result{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"set"::: ) , F6() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ), F8() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 5) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F6 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k8_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) ($#k8_finseq_4 :::"*>"::: ) ) "," (Set F8 "(" ")" ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k8_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) ($#k8_finseq_4 :::"*>"::: ) ) "," (Set F8 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) ")" )))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 5) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F6 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F8 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) ($#k10_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) ")" ))) ")" )) proof end; begin theorem :: CIRCCMB3:35 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))))))))) ; theorem :: CIRCCMB3:36 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "X2")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S")))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")))))))))) ; theorem :: CIRCCMB3:37 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))))) ; theorem :: CIRCCMB3:38 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:39 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:40 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))))) ; theorem :: CIRCCMB3:41 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k2_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:42 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k2_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:43 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:44 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:45 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:46 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: CIRCCMB3:47 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))))) ; begin theorem :: CIRCCMB3:48 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set (Var "X")) "," (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "st" (Bool (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A")) ($#k7_circcmb3 :::"+*"::: ) (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" ) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))))) "holds" (Bool (Set ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k2_circcmb3 :::"stabilization-time"::: ) (Set (Var "s9")) ")" ))))))))))) ; scheme :: CIRCCMB3:sch 14 Comb1CircResult{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set F2 "(" ")" ), F5() -> ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ), F6() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F2 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set F5 "(" ")" ) ($#k7_circcmb3 :::"+*"::: ) (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set F6 "(" ")" ) ")" ")" ) ")" ) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F5 "(" ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F4 "(" ")" ))))) "holds" (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F4 "(" ")" )))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F4 "(" ")" ))))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" ) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set F6 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "a1")) ")" ))))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F2 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F6 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a1")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "a1")) ")" ))) ")" )) and (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F4 "(" ")" )))) proof end; scheme :: CIRCCMB3:sch 15 Comb2CircResult{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5() -> ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set F3 "(" ")" ), F6() -> ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set F3 "(" ")" ) "," (Set F5 "(" ")" ), F7() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F3 "(" ")" ) ")" ) "," (Set F3 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set F6 "(" ")" ) ($#k7_circcmb3 :::"+*"::: ) (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set F7 "(" ")" ) ")" ")" ) ")" ) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F6 "(" ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F5 "(" ")" ))))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F5 "(" ")" )))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F5 "(" ")" ))))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F5 "(" ")" )))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F5 "(" ")" ))))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" ) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set F7 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" ))))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F3 "(" ")" ) ")" ) "," (Set F3 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F7 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" ))) ")" )) and (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set F7 "(" ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F5 "(" ")" )))) proof end; scheme :: CIRCCMB3:sch 16 Comb3CircResult{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ), F6() -> ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set F4 "(" ")" ), F7() -> ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set F4 "(" ")" ) "," (Set F6 "(" ")" ), F8() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F4 "(" ")" ) ")" ) "," (Set F4 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set F7 "(" ")" ) ($#k7_circcmb3 :::"+*"::: ) (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set F8 "(" ")" ) ")" ")" ) ")" ) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F7 "(" ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F6 "(" ")" ))))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) "st" (Bool "(" (Bool (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F6 "(" ")" )))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F6 "(" ")" ))))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F6 "(" ")" )))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F6 "(" ")" ))))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F6 "(" ")" )))) "implies" (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F6 "(" ")" ))))) "implies" (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) ")" ) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set F8 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" ))))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F4 "(" ")" ) ")" ) "," (Set F4 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F8 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" ))) ")" )) and (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set F8 "(" ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F6 "(" ")" )))) proof end; scheme :: CIRCCMB3:sch 17 Comb4CircResult{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ), F7() -> ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set F5 "(" ")" ), F8() -> ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set F5 "(" ")" ) "," (Set F7 "(" ")" ), F9() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 4) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F5 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set F8 "(" ")" ) ($#k7_circcmb3 :::"+*"::: ) (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k7_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k7_finseq_4 :::"*>"::: ) ) "," (Set F9 "(" ")" ) ")" ")" ) ")" ) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F8 "(" ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F7 "(" ")" ))))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ) "st" (Bool "(" (Bool (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" )))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" ))))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" )))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" ))))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" )))) "implies" (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" ))))) "implies" (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) ")" & "(" (Bool (Bool (Set F4 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" )))) "implies" (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F4 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F7 "(" ")" ))))) "implies" (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) ")" ) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k7_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k7_finseq_4 :::"*>"::: ) ) "," (Set F9 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ")" ))))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 4) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F5 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F9 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k9_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ($#k9_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ")" ))) ")" )) and (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k7_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k7_finseq_4 :::"*>"::: ) ) "," (Set F9 "(" ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F7 "(" ")" )))) proof end; scheme :: CIRCCMB3:sch 18 Comb5CircResult{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"set"::: ) , F6() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ), F8() -> ($#v8_struct_0 :::"finite"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set F6 "(" ")" ), F9() -> ($#m2_circcmb3 :::"Circuit"::: ) "of" (Set F6 "(" ")" ) "," (Set F8 "(" ")" ), F10() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 5) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F6 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set F9 "(" ")" ) ($#k7_circcmb3 :::"+*"::: ) (Set "(" ($#k5_circcmb3 :::"1GateCircuit"::: ) "(" (Set ($#k8_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) ($#k8_finseq_4 :::"*>"::: ) ) "," (Set F10 "(" ")" ) ")" ")" ) ")" ) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F9 "(" ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F8 "(" ")" ))))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ) "st" (Bool "(" (Bool (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" )))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" ))))) "implies" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F1 "(" ")" ))) ")" & "(" (Bool (Bool (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" )))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" ))))) "implies" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F2 "(" ")" ))) ")" & "(" (Bool (Bool (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" )))) "implies" (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" ))))) "implies" (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) ")" & "(" (Bool (Bool (Set F4 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" )))) "implies" (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F4 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" ))))) "implies" (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) ")" & "(" (Bool (Bool (Set F5 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" )))) "implies" (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set F5 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F8 "(" ")" ))))) "implies" (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) ")" ) "holds" (Bool (Set (Set "(" ($#k1_circcmb3 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k8_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) ($#k8_finseq_4 :::"*>"::: ) ) "," (Set F10 "(" ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) ")" ))))) provided (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 5) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set F6 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set F10 "(" ")" )) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F6 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) ($#k10_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) ")" ))) ")" )) and (Bool (Bool "not" (Set ($#k3_circcmb3 :::"Output"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k8_finseq_4 :::"<*"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) ($#k8_finseq_4 :::"*>"::: ) ) "," (Set F10 "(" ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F8 "(" ")" )))) proof end; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "S" is :::"with_nonpair_inputs"::: means :: CIRCCMB3:def 11 (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) "S") "is" ($#v1_facirc_1 :::"without_pairs"::: ) ); end; :: deftheorem defines :::"with_nonpair_inputs"::: CIRCCMB3:def 11 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ) "iff" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" )); registration cluster (Set ($#k4_ordinal1 :::"NAT"::: ) ) -> ($#v1_facirc_1 :::"without_pairs"::: ) ; let "X" be ($#v1_facirc_1 :::"without_pairs"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_facirc_1 :::"without_pairs"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) -> ($#v2_facirc_1 :::"nonpair-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) bbbadV4_CARD_3() ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_finset_1 :::"finite"::: ) bbbadV3_CARD_1("n") ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) bbbadV4_CARD_3() ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "p" be ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSequence":::); let "f" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msualg_1 :::"strict"::: ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#v4_circcmb3 :::"one-gate"::: ) ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msualg_1 :::"strict"::: ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#v4_circcmb3 :::"one-gate"::: ) ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) for ($#m1_circcmb3 :::"Signature"::: ) "of" "X"; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k2_msafree2 :::"InputVertices"::: ) "S") -> ($#v1_facirc_1 :::"without_pairs"::: ) ; end; theorem :: CIRCCMB3:49 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_xtuple_0 :::"pair"::: ) )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S")))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k3_msafree2 :::"InnerVertices"::: ) "S") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k3_msafree2 :::"InnerVertices"::: ) "S") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; theorem :: CIRCCMB3:50 (Bool "for" (Set (Var "x")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))))) ; theorem :: CIRCCMB3:51 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" "not" (Bool (Set (Var "x1")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) "is" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x1" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) "x1" ($#k12_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x1" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) "x1" ($#k9_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; theorem :: CIRCCMB3:52 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" "not" (Bool (Set (Var "x1")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" "not" (Bool (Set (Var "x2")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) "is" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x1" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); let "n2" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x1" "," "n2" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "n2" "," "x1" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x1", "x2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) "x1" "," "x2" ($#k2_finseq_4 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; theorem :: CIRCCMB3:53 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" "not" (Bool (Set (Var "x1")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" "not" (Bool (Set (Var "x2")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ")" ) & (Bool "(" (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" "not" (Bool (Set (Var "x3")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "S")) ($#k6_circcmb3 :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) "is" ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x1", "x2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); let "n" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "x1" "," "x2" "," "n" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "x1" "," "n" "," "x2" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "n" "," "x1" "," "x2" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); let "n1", "n2" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "x" "," "n1" "," "n2" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "n1" "," "x" "," "n2" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "n1" "," "n2" "," "x" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ($#m1_circcmb3 :::"Signature"::: ) "of" (Set (Const "X")); let "x1", "x2", "x3" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); cluster (Set "S" ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_circcmb3 :::"1GateCircStr"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) "x1" "," "x2" "," "x3" ($#k3_finseq_4 :::"*>"::: ) ) "," "f" ")" ")" )) -> ($#v6_circcmb3 :::"with_nonpair_inputs"::: ) ; end;