:: CIRCCOMB semantic presentation begin definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode Gate of "S" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"); end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "A")); let "g" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "B")); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> (Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "A")); let "g" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "B")); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> (Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for(Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k16_funcop_1 :::".-->"::: ) "B") -> (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k16_funcop_1 :::".-->"::: ) "B") -> (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for(Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k16_funcop_1 :::".-->"::: ) "B") -> bbbadV2_RELAT_1() ; end; theorem :: CIRCCOMB:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_finseq_2 :::"#"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k6_finseq_2 :::"#"::: ) ))))) ; theorem :: CIRCCOMB:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Y")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "f1", "g1" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "A")); let "B" be ($#m1_hidden :::"set"::: ) ; let "f2", "g2" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "B")); let "h1" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "f1")) "," (Set (Const "g1")); let "h2" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "f2")) "," (Set (Const "g2")); :: original: :::"+*"::: redefine func "h1" :::"+*"::: "h2" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "f1" ($#k1_funct_4 :::"+*"::: ) "f2") "," (Set "g1" ($#k1_funct_4 :::"+*"::: ) "g2"); end; definitionlet "S1", "S2" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; pred "S1" :::"tolerates"::: "S2" means :: CIRCCOMB:def 1 (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S1") ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S2")) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S1") ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S2")) ")" ); reflexivity (Bool "for" (Set (Var "S1")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1")))) ")" )) ; symmetry (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))))) "holds" (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1")))) ")" )) ; end; :: deftheorem defines :::"tolerates"::: CIRCCOMB:def 1 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2")))) ")" ) ")" )); definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func "S1" :::"+*"::: "S2" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: CIRCCOMB:def 2 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S2"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S2"))) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S1") ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S2"))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S1") ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S2"))) ")" ); end; :: deftheorem defines :::"+*"::: CIRCCOMB:def 2 : (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 "b3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2"))))) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2"))))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))))) ")" ) ")" ))); theorem :: CIRCCOMB:3 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "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 (Var "S2")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S3"))) & (Bool (Set (Var "S3")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S1")))) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S3")))) ; theorem :: CIRCCOMB:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) "#)" ))) ; theorem :: CIRCCOMB:5 (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")))) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S1"))))) ; theorem :: CIRCCOMB:6 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ) ($#k2_circcomb :::"+*"::: ) (Set (Var "S3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set "(" (Set (Var "S2")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S3")) ")" )))) ; theorem :: CIRCCOMB:7 (Bool "for" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set (Var "f"))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))) ($#r1_tarski :::"c="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v2_msafree2 :::"Circuit-like"::: ) ))) ; theorem :: CIRCCOMB:8 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))))) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v2_msafree2 :::"Circuit-like"::: ) )) ; theorem :: CIRCCOMB:9 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "S1")) "is" ($#v11_struct_0 :::"void"::: ) ) "or" "not" (Bool (Set (Var "S2")) "is" ($#v11_struct_0 :::"void"::: ) ) ")" )) "holds" (Bool "not" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v11_struct_0 :::"void"::: ) ))) ; theorem :: CIRCCOMB:10 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v8_struct_0 :::"finite"::: ) )) ; registrationlet "S1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; cluster (Set "S2" ($#k2_circcomb :::"+*"::: ) "S1") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; end; theorem :: CIRCCOMB:11 (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")))) "holds" (Bool "(" (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")) ")" ))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")) ")" ))) ")" )) ; theorem :: CIRCCOMB:12 (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 "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )))) "holds" (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")))))) ; theorem :: CIRCCOMB:13 (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")))) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )))) "holds" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")))))) ; theorem :: CIRCCOMB:14 (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "o")))) "holds" (Bool "(" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2")))) ")" ))))) ; theorem :: CIRCCOMB:15 (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S")))) & (Bool (Set ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v2")))) ")" ))))) ; theorem :: CIRCCOMB:16 (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (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")))) "holds" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "o")))) "holds" (Bool "(" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1")))) ")" ))))) ; theorem :: CIRCCOMB:17 (Bool "for" (Set (Var "S1")) "," (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 "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 (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S")))) & (Bool (Set ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v1")))) ")" ))))) ; begin definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A1" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S1")); let "A2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); pred "A1" :::"tolerates"::: "A2" means :: CIRCCOMB:def 3 (Bool "(" (Bool "S1" ($#r1_circcomb :::"tolerates"::: ) "S2") & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A1") ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A2")) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "A1") ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "A2")) ")" ); end; :: deftheorem defines :::"tolerates"::: CIRCCOMB:def 3 : (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 "A1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) "iff" (Bool "(" (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2"))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2")))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A2")))) ")" ) ")" )))); definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A1" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S1")); let "A2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); assume (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A2")))) ; func "A1" :::"+*"::: "A2" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") means :: CIRCCOMB:def 4 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A1") ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A2"))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "A1") ($#k1_circcomb :::"+*"::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "A2"))) ")" ); end; :: deftheorem defines :::"+*"::: CIRCCOMB:def 4 : (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 "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")))) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A1"))) ($#k1_circcomb :::"+*"::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A2"))))) ")" ) ")" ))))); theorem :: CIRCCOMB:18 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Var "A")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A"))))) ; theorem :: CIRCCOMB:19 (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"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))) "holds" (Bool (Set (Var "A2")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A1")))))) ; theorem :: CIRCCOMB:20 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "A3")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S3")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A2")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A3"))) & (Bool (Set (Var "A3")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A1")))) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A3"))))))) ; theorem :: CIRCCOMB:21 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) "#)" )))) ; theorem :: CIRCCOMB: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 "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A1"))))))) ; theorem :: CIRCCOMB:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "A3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S3")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2")))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A3")))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A3"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))))) "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 :: CIRCCOMB:24 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) "is" ($#v4_msafree2 :::"finite-yielding"::: ) )))) ; theorem :: CIRCCOMB:25 (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 "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1")))) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2")))) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "s2"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ))))))))) ; theorem :: CIRCCOMB:26 (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 "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "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")))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))))) & (Bool (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) ")" ))))) ; theorem :: CIRCCOMB:27 (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"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o2")))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set (Var "A2")) ")" ))))))) ; theorem :: CIRCCOMB: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"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2")))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o1")))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," (Set (Var "A1")) ")" ))))))) ; theorem :: CIRCCOMB:29 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (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 "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "g2")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s2")))))))))))) ; theorem :: CIRCCOMB:30 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "g1")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s1")))))))))))) ; theorem :: CIRCCOMB:31 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) "holds" (Bool "(" (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"))))) & (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")))) "or" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) & (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"))))) & (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) "or" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S")))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ))))))) ; theorem :: CIRCCOMB:32 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (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 ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" )))))))))) ; theorem :: CIRCCOMB:33 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (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 ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1")) ")" )))))))))) ; theorem :: CIRCCOMB:34 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (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 ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1")) ")" )))))))))) ; theorem :: CIRCCOMB:35 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (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 ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" )))))))))) ; begin definitionlet "f" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; func :::"1GateCircStr"::: "(" "p" "," "f" "," "x" ")" -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: CIRCCOMB:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "p" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) "p") & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) "x") ")" ); end; :: deftheorem defines :::"1GateCircStr"::: CIRCCOMB:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b4"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b4"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ))))); registrationlet "f" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" "," "x" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; end; theorem :: CIRCCOMB:36 (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 "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "p")) "," (Set (Var "f")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "p")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "p")) "," (Set (Var "f")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "x")))) ")" ))) ; theorem :: CIRCCOMB:37 (Bool "for" (Set (Var "f")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; theorem :: CIRCCOMB:38 (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 ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; definitionlet "f" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); func :::"1GateCircStr"::: "(" "p" "," "f" ")" -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: CIRCCOMB:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "p" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) "p") & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ")" ); end; :: deftheorem defines :::"1GateCircStr"::: CIRCCOMB:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b3")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ")" ) ")" )))); registrationlet "f" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; end; theorem :: CIRCCOMB:39 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ")" )))) ; theorem :: CIRCCOMB:40 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "p")) "," (Set (Var "f")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "p")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "p")) "," (Set (Var "f")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))) ")" ))) ; theorem :: CIRCCOMB:41 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" )))) ; theorem :: CIRCCOMB:42 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: CIRCCOMB:43 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_circcomb :::"tolerates"::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )))) ; begin definitionlet "IT" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "IT" is :::"unsplit"::: means :: CIRCCOMB:def 7 (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "IT") ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT"))); attr "IT" is :::"gate`1=arity"::: means :: CIRCCOMB:def 8 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT"))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "g")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ))); attr "IT" is :::"gate`2isBoolean"::: means :: CIRCCOMB:def 9 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT"))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "g")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))))); end; :: deftheorem defines :::"unsplit"::: CIRCCOMB:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_circcomb :::"unsplit"::: ) ) "iff" (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT"))))) ")" )); :: deftheorem defines :::"gate`1=arity"::: CIRCCOMB:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT"))))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "g")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" )); :: deftheorem defines :::"gate`2isBoolean"::: CIRCCOMB:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) ) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "g")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))))) ")" )); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "IT" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "IT" is :::"gate`2=den"::: means :: CIRCCOMB:def 10 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "g")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"gate`2=den"::: CIRCCOMB:def 10 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "g")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "g")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "IT" is :::"gate`2=den"::: means :: CIRCCOMB:def 11 (Bool "ex" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "IT" "st" (Bool (Set (Var "A")) "is" ($#v4_circcomb :::"gate`2=den"::: ) )); end; :: deftheorem defines :::"gate`2=den"::: CIRCCOMB:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_circcomb :::"gate`2=den"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IT")) "st" (Bool (Set (Var "A")) "is" ($#v4_circcomb :::"gate`2=den"::: ) )) ")" )); scheme :: CIRCCOMB:sch 1 MSSLambdaWeak{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) proof end; scheme :: CIRCCOMB:sch 2 Lemma{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "A")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set F1 "(" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "g")) "," (Set (Var "p")) ")" ))) ")" ) ")" )) provided (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set F1 "(" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))))) "holds" (Bool (Set F2 "(" (Set (Var "g")) "," (Set (Var "p")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )))) proof end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_circcomb :::"gate`2isBoolean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_circcomb :::"gate`2=den"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; theorem :: CIRCCOMB:44 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_circcomb :::"unsplit"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "o")))) ")" )) ; theorem :: CIRCCOMB:45 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_circcomb :::"unsplit"::: ) )) "holds" (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; theorem :: CIRCCOMB:46 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#v1_circcomb :::"unsplit"::: ) ) & (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) ")" ))) ; registrationlet "f" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ; end; registration cluster ($#~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"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; theorem :: CIRCCOMB:47 (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 (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2")))) ; theorem :: CIRCCOMB:48 (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 "A1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v4_circcomb :::"gate`2=den"::: ) )) "holds" (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A2"))))))) ; theorem :: CIRCCOMB:49 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v1_circcomb :::"unsplit"::: ) )) ; registrationlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ; end; theorem :: CIRCCOMB:50 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v2_circcomb :::"gate`1=arity"::: ) )) ; registrationlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ; end; theorem :: CIRCCOMB:51 (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")) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) ) & (Bool (Set (Var "S2")) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) )) "holds" (Bool (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) )) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); mode FinSeqLen of "n" is "n" ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "Y")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); let "x" be ($#m1_hidden :::"set"::: ) ; assume "(" (Bool (Bool (Set (Const "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Const "p"))))) "implies" (Bool (Set (Const "X")) ($#r1_hidden :::"="::: ) (Set (Const "Y"))) ")" ; func :::"1GateCircuit"::: "(" "p" "," "f" "," "x" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" "," "x" ")" ) means :: CIRCCOMB:def 12 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "p" ")" ) ($#k7_funcop_1 :::"-->"::: ) "X" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "x" ($#k16_funcop_1 :::".-->"::: ) "Y" ")" ))) & (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) "f") ")" ); end; :: deftheorem defines :::"1GateCircuit"::: CIRCCOMB:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" ) "holds" (Bool "for" (Set (Var "b7")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k4_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k6_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "X")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "b7"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ) ")" ))))))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); func :::"1GateCircuit"::: "(" "p" "," "f" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) means :: CIRCCOMB:def 13 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ")" )) ($#k7_funcop_1 :::"-->"::: ) "X")) & (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "p" "," "f" ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) "f") ")" ); end; :: deftheorem defines :::"1GateCircuit"::: CIRCCOMB:def 13 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b5")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b5"))) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "X")))) & (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "b5"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ) ")" )))))); theorem :: CIRCCOMB:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#v5_circcomb :::"gate`2=den"::: ) ) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); cluster (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" "p" "," "f" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ; cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v5_circcomb :::"gate`2=den"::: ) ; end; theorem :: CIRCCOMB:53 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); cluster (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ) -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_circcomb :::"gate`2isBoolean"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registrationlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "S1" ($#k2_circcomb :::"+*"::: ) "S2") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ; end; theorem :: CIRCCOMB:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "p")) "," (Set (Var "f")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); cluster (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" "p" "," "f" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ; end; theorem :: CIRCCOMB:55 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r2_circcomb :::"tolerates"::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )))))) ; theorem :: CIRCCOMB:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#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")) ")" )))))))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "IT" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "IT" is :::"Boolean"::: means :: CIRCCOMB:def 14 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "S" "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ))); end; :: deftheorem defines :::"Boolean"::: CIRCCOMB:def 14 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_circcomb :::"Boolean"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ))) ")" ))); theorem :: CIRCCOMB:57 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_circcomb :::"Boolean"::: ) ) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ))) ")" ))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v6_circcomb :::"Boolean"::: ) -> ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; theorem :: CIRCCOMB:58 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_circcomb :::"Boolean"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: CIRCCOMB:59 (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 "A1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v6_circcomb :::"Boolean"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v6_circcomb :::"Boolean"::: ) )) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))))) ; theorem :: CIRCCOMB:60 (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 "A1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v6_circcomb :::"Boolean"::: ) ) & (Bool (Set (Var "A1")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v6_circcomb :::"Boolean"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v4_circcomb :::"gate`2=den"::: ) )) "holds" (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2")))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v3_msualg_1 :::"strict"::: ) ($#v6_circcomb :::"Boolean"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; theorem :: CIRCCOMB:61 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) "is" ($#v6_circcomb :::"Boolean"::: ) )))) ; theorem :: CIRCCOMB:62 (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 "A1")) "being" ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) "is" ($#v6_circcomb :::"Boolean"::: ) )))) ; theorem :: CIRCCOMB:63 (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 "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v4_circcomb :::"gate`2=den"::: ) ) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))) "is" ($#v4_circcomb :::"gate`2=den"::: ) )))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#v5_circcomb :::"gate`2=den"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A1" be ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S1")); let "A2" be ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S2")); cluster (Set "A1" ($#k3_circcomb :::"+*"::: ) "A2") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#v4_circcomb :::"gate`2=den"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" "p" "," "f" ")" ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "X")) ")" ) "," (Set (Const "X")); let "p" be ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Const "n")); cluster (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" "p" "," "f" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ; end; theorem :: CIRCCOMB:64 (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")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ) "holds" (Bool "(" (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"))))) & (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")))) "or" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) & (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"))))) & (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) "or" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" )))))) ;