:: FACIRC_1 semantic presentation begin registration cluster ($#v1_xtuple_0 :::"pair"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster bbbadV7_ORDINAL1() -> ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; definitioncanceled; let "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"with_pair"::: means :: FACIRC_1:def 2 (Bool "ex" (Set (Var "x")) "being" ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem FACIRC_1:def 1 : canceled; :: deftheorem defines :::"with_pair"::: FACIRC_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_facirc_1 :::"with_pair"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )); notationlet "IT" be ($#m1_hidden :::"set"::: ) ; antonym :::"without_pairs"::: "IT" for :::"with_pair"::: ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_facirc_1 :::"without_pairs"::: ) for ($#m1_hidden :::"set"::: ) ; let "x" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) -> ($#v1_facirc_1 :::"without_pairs"::: ) ; let "y" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "x" "," "y" ($#k2_tarski :::"}"::: ) ) -> ($#v1_facirc_1 :::"without_pairs"::: ) ; let "z" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "x" "," "y" "," "z" ($#k1_enumset1 :::"}"::: ) ) -> ($#v1_facirc_1 :::"without_pairs"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_facirc_1 :::"without_pairs"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X", "Y" be ($#v1_facirc_1 :::"without_pairs"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v1_facirc_1 :::"without_pairs"::: ) ; end; registrationlet "X" be ($#v1_facirc_1 :::"without_pairs"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v1_facirc_1 :::"without_pairs"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v1_facirc_1 :::"without_pairs"::: ) ; cluster (Set "Y" ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v1_facirc_1 :::"without_pairs"::: ) ; end; registrationlet "x" be ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ; let "y" be ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "x" "," "y" ($#k2_tarski :::"}"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ; let "z" be ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "x" "," "y" "," "z" ($#k1_enumset1 :::"}"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_facirc_1 :::"without_pairs"::: ) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::"nonpair-yielding"::: means :: FACIRC_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool "not" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xtuple_0 :::"pair"::: ) ))); end; :: deftheorem defines :::"nonpair-yielding"::: FACIRC_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool "not" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xtuple_0 :::"pair"::: ) ))) ")" )); registrationlet "x" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "x" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v2_facirc_1 :::"nonpair-yielding"::: ) ; let "y" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v2_facirc_1 :::"nonpair-yielding"::: ) ; let "z" be ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "x" "," "y" "," "z" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v2_facirc_1 :::"nonpair-yielding"::: ) ; end; theorem :: FACIRC_1:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_facirc_1 :::"nonpair-yielding"::: ) )) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"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"::: ) ($#v4_card_3 :::"countable"::: ) ($#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"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_facirc_1 :::"nonpair-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "f") -> ($#v1_facirc_1 :::"without_pairs"::: ) ; end; theorem :: FACIRC_1:2 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2"))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) "is" ($#m1_hidden :::"Relation":::))) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FACIRC_1:3 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) "is" ($#m1_hidden :::"Relation":::))) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FACIRC_1:4 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2"))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")) ")" ) ")" ))) ")" )) ; theorem :: FACIRC_1:5 (Bool "for" (Set (Var "X")) "," (Set (Var "R")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) & (Bool (Set (Var "R")) "is" ($#m1_hidden :::"Relation":::))) "holds" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "R")))) ; theorem :: FACIRC_1:6 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) "is" ($#m1_hidden :::"Relation":::))) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")) ")" ) ")" ))) ")" )) ; theorem :: FACIRC_1:7 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) "is" ($#m1_hidden :::"Relation":::))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")) ")" )))) ; theorem :: FACIRC_1:8 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2"))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: FACIRC_1:9 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; begin definitionlet "i" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode Tuple of "i" "," "D" is ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; scheme :: FACIRC_1:sch 1 2AryBooleEx{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) proof end; scheme :: FACIRC_1:sch 2 2AryBooleUniq{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: FACIRC_1:sch 3 2AryBooleDef{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) } : (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (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 ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" ) proof end; scheme :: FACIRC_1:sch 4 3AryBooleEx{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )))) proof end; scheme :: FACIRC_1:sch 5 3AryBooleUniq{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (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 ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: FACIRC_1:sch 6 3AryBooleDef{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) } : (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (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 ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (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 ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" ) proof end; definitionfunc :::"'xor'"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: FACIRC_1:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y"))))); func :::"'or'"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: FACIRC_1:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y"))))); func :::"'&'"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: FACIRC_1:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"'xor'"::: FACIRC_1:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_facirc_1 :::"'xor'"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"'or'"::: FACIRC_1:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_facirc_1 :::"'or'"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"'&'"::: FACIRC_1:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_facirc_1 :::"'&'"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y"))))) ")" )); definitionfunc :::"or3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: FACIRC_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))); end; :: deftheorem defines :::"or3"::: FACIRC_1:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_facirc_1 :::"or3"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))) ")" )); begin theorem :: FACIRC_1:10 (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 "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "g")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g")) ")" ) ")" ))))))) ; 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")); let "n" be ($#m1_hidden :::"Nat":::); func :::"Following"::: "(" "s" "," "n" ")" -> ($#m1_subset_1 :::"State":::) "of" "A" means :: FACIRC_1:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "s") & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"Following"::: FACIRC_1:def 8 : (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_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" ) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )) ")" )))))); theorem :: FACIRC_1:11 (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 (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s")))))) ; theorem :: FACIRC_1:12 (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_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: FACIRC_1:13 (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")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "m")) ")" )))))) ; theorem :: FACIRC_1:14 (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 (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))))))) ; theorem :: FACIRC_1:15 (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 (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" )))))) ; theorem :: FACIRC_1:16 (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_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set "(" ($#k6_circuit2 :::"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")); let "x" be ($#m1_hidden :::"set"::: ) ; pred "s" :::"is_stable_at"::: "x" means :: FACIRC_1:def 9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" "s" "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) "x") ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) "x"))); end; :: deftheorem defines :::"is_stable_at"::: FACIRC_1:def 9 : (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"::: ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"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"))))) ")" ))))); theorem :: FACIRC_1:17 (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 "s")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "x")))))))) ; theorem :: FACIRC_1:18 (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 (Set (Var "s")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "x"))))))) ; theorem :: FACIRC_1:19 (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 "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Var "s")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "g")))))))) ; begin theorem :: FACIRC_1:20 (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 "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "S2")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S1")) ")" ))) ")" ))) ; theorem :: FACIRC_1:21 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "S2")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S1")) ")" ))) ")" ))) ; theorem :: FACIRC_1:22 (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 "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))))) ; theorem :: FACIRC_1:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S1"))))) ; theorem :: FACIRC_1:24 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A1"))))))) ; theorem :: FACIRC_1:25 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "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"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A3")) "being" ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S3")) "holds" (Bool (Set (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) ($#k3_circcomb :::"+*"::: ) (Set (Var "A3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set "(" (Set (Var "A2")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A3")) ")" ))))))) ; theorem :: FACIRC_1:26 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) "is" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1"))) & (Bool (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) "is" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2"))) ")" ))))) ; theorem :: FACIRC_1:27 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")) ")" )))) ; theorem :: FACIRC_1:28 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (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")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1"))))))))) ; theorem :: FACIRC_1:29 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (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")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2"))))))))) ; theorem :: FACIRC_1:30 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (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")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" )))))))) ; theorem :: FACIRC_1:31 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (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")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" )))))))) ; theorem :: FACIRC_1:32 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (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")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))))))))))) ; theorem :: FACIRC_1:33 (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"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (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")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))))))))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_circcomb :::"gate`2=den"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "g" be ($#m1_subset_1 :::"Gate":::) "of" (Set (Const "S")); cluster (Set "g" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FACIRC_1:34 (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"::: ) ($#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 "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g")) ")" ) ")" ))))))) ; theorem :: FACIRC_1:35 (Bool "for" (Set (Var "S")) "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"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#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 "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: FACIRC_1:36 (Bool "for" (Set (Var "S")) "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"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#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 "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "s")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))))))) ; theorem :: FACIRC_1:37 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) ; begin theorem :: FACIRC_1:38 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)))) ; theorem :: FACIRC_1:39 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ))) ; theorem :: FACIRC_1:40 (Bool "for" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: FACIRC_1:41 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ))) ; theorem :: FACIRC_1:42 (Bool "for" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: FACIRC_1:43 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))) ")" )) ; theorem :: FACIRC_1:44 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))) ")" )) ; theorem :: FACIRC_1:45 (Bool "for" (Set (Var "f")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" ))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" ))) ; theorem :: FACIRC_1:46 (Bool "for" (Set (Var "f")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) & (Bool (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ) "is" ($#v2_msafree2 :::"Circuit-like"::: ) ) ")" ))) ; theorem :: FACIRC_1:47 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ))))) ; definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"1GateCircuit"::: "(" "x" "," "y" "," "f" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ")" ) equals :: FACIRC_1:def 10 (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ")" ); end; :: deftheorem defines :::"1GateCircuit"::: FACIRC_1:def 10 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" )))); theorem :: FACIRC_1:48 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ))))) ; theorem :: FACIRC_1:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) ))))) ; theorem :: FACIRC_1:50 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" )))) ; theorem :: FACIRC_1:51 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; definitionlet "x", "y", "z" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"1GateCircuit"::: "(" "x" "," "y" "," "z" "," "f" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "x" "," "y" "," "z" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ) equals :: FACIRC_1:def 11 (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) "x" "," "y" "," "z" ($#k11_finseq_1 :::"*>"::: ) ) "," "f" ")" ); end; :: deftheorem defines :::"1GateCircuit"::: FACIRC_1:def 11 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" )))); theorem :: FACIRC_1:52 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "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_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")) ")" ) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")))) ")" ))))) ; theorem :: FACIRC_1:53 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "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_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) ))))) ; theorem :: FACIRC_1:54 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")) ")" ) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")))) ")" )))) ; theorem :: FACIRC_1:55 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; begin definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"2GatesCircStr"::: "(" "x" "," "y" "," "c" "," "f" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FACIRC_1:def 12 (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ($#k4_tarski :::"]"::: ) ) "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ")" ")" )); end; :: deftheorem defines :::"2GatesCircStr"::: FACIRC_1:def 12 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ")" ")" ))))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"2GatesCircOutput"::: "(" "x" "," "y" "," "c" "," "f" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," "f" ")" ")" )) equals :: FACIRC_1:def 13 (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ($#k4_tarski :::"]"::: ) ) "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"2GatesCircOutput"::: FACIRC_1:def 13 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )))); registrationlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); cluster (Set ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" "x" "," "y" "," "c" "," "f" ")" ) -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: FACIRC_1:56 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ) ($#k2_tarski :::"}"::: ) )))) ; theorem :: FACIRC_1:57 (Bool "for" (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) )))) ; definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"2GatesCircuit"::: "(" "x" "," "y" "," "c" "," "f" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," "f" ")" ) equals :: FACIRC_1:def 14 (Set (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "x" "," "y" "," "f" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," "f" ($#k4_tarski :::"]"::: ) ) "," "c" "," "f" ")" ")" )); end; :: deftheorem defines :::"2GatesCircuit"::: FACIRC_1:def 14 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "f")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ))))); theorem :: FACIRC_1:58 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)))) ; theorem :: FACIRC_1:59 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ))) ; theorem :: FACIRC_1:60 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ))) ")" ))) ; theorem :: FACIRC_1:61 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ))) ")" ))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "A")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); :: original: :::"."::: redefine func "s" :::"."::: "v" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; theorem :: FACIRC_1:62 (Bool "for" (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )))) ; theorem :: FACIRC_1:63 (Bool "for" (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set (Var "f")) ")" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; theorem :: FACIRC_1:64 (Bool "for" (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3"))))))) ; theorem :: FACIRC_1:65 (Bool "for" (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_facirc_1 :::"'or'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k2_facirc_1 :::"'or'"::: ) ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k2_facirc_1 :::"'or'"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_binarith :::"'or'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "a3"))))))) ; theorem :: FACIRC_1:66 (Bool "for" (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; begin definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitAdderOutput"::: "(" "x" "," "y" "," "c" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" )) equals :: FACIRC_1:def 15 (Set ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ); end; :: deftheorem defines :::"BitAdderOutput"::: FACIRC_1:def 15 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitAdderCirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ) equals :: FACIRC_1:def 16 (Set ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ); end; :: deftheorem defines :::"BitAdderCirc"::: FACIRC_1:def 16 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_facirc_1 :::"BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"MajorityIStr"::: "(" "x" "," "y" "," "c" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FACIRC_1:def 17 (Set (Set "(" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "c" "," "x" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" )); end; :: deftheorem defines :::"MajorityIStr"::: FACIRC_1:def 17 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_facirc_1 :::"MajorityIStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" )))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"MajorityStr"::: "(" "x" "," "y" "," "c" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FACIRC_1:def 18 (Set (Set "(" ($#k14_facirc_1 :::"MajorityIStr"::: ) "(" "x" "," "y" "," "c" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "c" "," "x" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )); end; :: deftheorem defines :::"MajorityStr"::: FACIRC_1:def 18 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_facirc_1 :::"MajorityIStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"MajorityICirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k14_facirc_1 :::"MajorityIStr"::: ) "(" "x" "," "y" "," "c" ")" ) equals :: FACIRC_1:def 19 (Set (Set "(" (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "x" "," "y" "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "y" "," "c" "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "c" "," "x" "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" )); end; :: deftheorem defines :::"MajorityICirc"::: FACIRC_1:def 19 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k16_facirc_1 :::"MajorityICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" ) ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "c")) "," (Set (Var "x")) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ")" ")" )))); theorem :: FACIRC_1:67 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FACIRC_1:68 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: FACIRC_1:69 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k16_facirc_1 :::"MajorityICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "b"))))))) ; theorem :: FACIRC_1:70 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k16_facirc_1 :::"MajorityICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "b"))))))) ; theorem :: FACIRC_1:71 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k16_facirc_1 :::"MajorityICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "b"))))))) ; definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"MajorityOutput"::: "(" "x" "," "y" "," "c" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" "x" "," "y" "," "c" ")" ")" )) equals :: FACIRC_1:def 20 (Set ($#k4_tarski :::"["::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "c" "," "x" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"MajorityOutput"::: FACIRC_1:def 20 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ($#k4_tarski :::"]"::: ) ))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"MajorityCirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k15_facirc_1 :::"MajorityStr"::: ) "(" "x" "," "y" "," "c" ")" ) equals :: FACIRC_1:def 21 (Set (Set "(" ($#k16_facirc_1 :::"MajorityICirc"::: ) "(" "x" "," "y" "," "c" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "c" "," "x" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )); end; :: deftheorem defines :::"MajorityCirc"::: FACIRC_1:def 21 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_facirc_1 :::"MajorityICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )))); theorem :: FACIRC_1:72 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FACIRC_1:73 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FACIRC_1:74 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FACIRC_1:75 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))) ")" )) ; theorem :: FACIRC_1:76 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2"))))))) ; theorem :: FACIRC_1:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; theorem :: FACIRC_1:78 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1"))))))) ; theorem :: FACIRC_1:79 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_binarith :::"'or'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "a3"))))))) ; theorem :: FACIRC_1:80 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2"))))))) ; theorem :: FACIRC_1:81 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; theorem :: FACIRC_1:82 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1"))))))) ; theorem :: FACIRC_1:83 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1")) ")" )))))) ; theorem :: FACIRC_1:84 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))) ; definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitAdderWithOverflowStr"::: "(" "x" "," "y" "," "c" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FACIRC_1:def 22 (Set (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" "x" "," "y" "," "c" ")" ")" )); end; :: deftheorem defines :::"BitAdderWithOverflowStr"::: FACIRC_1:def 22 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )))); theorem :: FACIRC_1:85 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: FACIRC_1:86 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FACIRC_1:87 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))) ; definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitAdderWithOverflowCirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" "x" "," "y" "," "c" ")" ) equals :: FACIRC_1:def 23 (Set (Set "(" ($#k13_facirc_1 :::"BitAdderCirc"::: ) "(" "x" "," "y" "," "c" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" "x" "," "y" "," "c" ")" ")" )); end; :: deftheorem defines :::"BitAdderWithOverflowCirc"::: FACIRC_1:def 23 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_facirc_1 :::"BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )))); theorem :: FACIRC_1:88 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FACIRC_1:89 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: FACIRC_1:90 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FACIRC_1:91 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1")) ")" ))) ")" )))) ; theorem :: FACIRC_1:92 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))) ;