:: CIRCCMB2 semantic presentation begin 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 ($#k7_circcomb :::"1GateCircuit"::: ) "(" "p" "," "f" ")" ) -> ($#v6_circcomb :::"Boolean"::: ) ; end; theorem :: CIRCCMB2:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_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 (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) (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 (Var "o")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")))))))))) ; theorem :: CIRCCMB2:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_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 (Var "X")) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) )))))) ; theorem :: CIRCCMB2:3 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))))))) ; theorem :: CIRCCMB2:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n1")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n2")))) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n1")) ")" )))))) ; begin scheme :: CIRCCMB2:sch 1 CIRCCMB29sch1{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) proof end; scheme :: CIRCCMB2:sch 2 CIRCCMB29sch2{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F3() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F4() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool P1[(Set (Var "S")) "," (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Var "n"))]) ")" ))) provided (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool P1[(Set (Var "S")) "," (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) )]) ")" ))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool P1[(Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n"))])) "holds" (Bool P1[(Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "," (Set F2 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "," (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))])))) proof end; scheme :: CIRCCMB2:sch 3 CIRCCMB29sch3{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F5() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )))) provided (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) proof end; scheme :: CIRCCMB2:sch 4 CIRCCMB29sch4{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) proof end; scheme :: CIRCCMB2:sch 5 CIRCCMB29sch5{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Nat":::) } : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) "holds" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Var "S2")))) proof end; scheme :: CIRCCMB2:sch 6 CIRCCMB29sch6{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Nat":::) } : (Bool "(" (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) "holds" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Var "S2"))) ")" ) ")" ) proof end; scheme :: CIRCCMB2:sch 7 CIRCCMB29sch7{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) provided (Bool "(" (Bool (Set F1 "(" ")" ) "is" ($#v1_circcomb :::"unsplit"::: ) ) & (Bool (Set F1 "(" ")" ) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) & (Bool (Set F1 "(" ")" ) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) ) & (Bool (Bool "not" (Set F1 "(" ")" ) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" (Set F1 "(" ")" ) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Set F1 "(" ")" ) "is" ($#v1_msualg_1 :::"strict"::: ) ) ")" ) and (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v1_circcomb :::"unsplit"::: ) ) & (Bool (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) & (Bool (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) ) & (Bool (Bool "not" (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Set F2 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v1_msualg_1 :::"strict"::: ) ) ")" )))) proof end; scheme :: CIRCCMB2:sch 8 CIRCCMB29sch8{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~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"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set F2 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) provided (Bool "(" (Bool (Set F1 "(" ")" ) "is" ($#v1_circcomb :::"unsplit"::: ) ) & (Bool (Set F1 "(" ")" ) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) & (Bool (Set F1 "(" ")" ) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) ) & (Bool (Bool "not" (Set F1 "(" ")" ) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" (Set F1 "(" ")" ) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Set F1 "(" ")" ) "is" ($#v1_msualg_1 :::"strict"::: ) ) ")" ) proof end; scheme :: CIRCCMB2:sch 9 CIRCCMB29sch9{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Nat":::) } : (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_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" ))) "holds" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Var "S2")))) proof end; begin theorem :: CIRCCMB2: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 ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")) ")" ) ")" )))) ; theorem :: CIRCCMB2:6 (Bool "for" (Set (Var "X")) "being" ($#v1_facirc_1 :::"without_pairs"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: CIRCCMB2:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "Y")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Z"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Z")))))) ; theorem :: CIRCCMB2:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Z"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Z")))))) ; scheme :: CIRCCMB2:sch 10 CIRCCMB29sch10{ F1() -> ($#~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"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~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"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "n")) ")" )) & (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set F4 "(" (Set "(" (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "n")) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" ))) provided (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" ")" )) "is" ($#m1_hidden :::"Relation":::)) and (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F1 "(" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) and (Bool "(" (Bool (Set F2 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" ")" ))) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) "is" ($#m1_hidden :::"Relation":::)))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "n")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set F2 "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) ")" )))) proof end; scheme :: CIRCCMB2:sch 11 CIRCCMB29sch11{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#~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"::: ) , F2() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~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"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F1 "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set F1 "(" (Set (Var "n")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set F3 "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "n")) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" (Set (Var "n")) ")" )) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F1 "(" (Set (Var "n")) ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" )) provided (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#m1_hidden :::"Relation":::)) and (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F1 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) and (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" ))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) "is" ($#m1_hidden :::"Relation":::)))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "n")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set F1 "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) ")" )))) proof end; begin scheme :: CIRCCMB2:sch 12 CIRCCMB29sch12{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" )) proof end; scheme :: CIRCCMB2:sch 13 CIRCCMB29sch13{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F5() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F6() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool P1[(Set (Var "S")) "," (Set (Var "A")) "," (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Var "n"))]) ")" )))) provided (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S"))(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool P1[(Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) )]) ")" )))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool P1[(Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n"))])) "holds" (Bool P1[(Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "," (Set F2 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "," (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "," (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))]))))) and (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F2 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; scheme :: CIRCCMB2:sch 14 CIRCCMB29sch14{ F1( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F5() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F6() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F7() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F8() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F9() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "(" (Bool (Set F4 "(" ")" ) ($#r8_pboole :::"="::: ) (Set F5 "(" ")" )) & (Bool (Set F6 "(" ")" ) ($#r8_pboole :::"="::: ) (Set F7 "(" ")" )) & (Bool (Set F8 "(" ")" ) ($#r8_pboole :::"="::: ) (Set F9 "(" ")" )) ")" ) provided (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))) and (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set F9 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F9 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F9 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))))) and (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F2 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; scheme :: CIRCCMB2:sch 15 CIRCCMB29sch15{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F7() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F8() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) provided (Bool "(" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set F8 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))))) and (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F4 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F3 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; scheme :: CIRCCMB2:sch 16 CIRCCMB29sch16{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F7() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S"))(Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F7 "(" ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F7 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" )))) provided (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F5 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; scheme :: CIRCCMB2:sch 17 CIRCCMB29sch17{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F4() -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F8() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F2 "(" ")" )(Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" ))) provided (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) and (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; scheme :: CIRCCMB2:sch 18 CIRCCMB29sch18{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F4() -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F8() -> ($#m1_hidden :::"Nat":::) } : (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F2 "(" ")" ) "st" (Bool (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" ))) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) provided (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; scheme :: CIRCCMB2:sch 19 CIRCCMB29sch19{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6() -> ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F8() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "A")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F2 "(" ")" )(Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" ))) provided (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v1_circcomb :::"unsplit"::: ) ) & (Bool (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v2_circcomb :::"gate`1=arity"::: ) ) & (Bool (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v3_circcomb :::"gate`2isBoolean"::: ) ) & (Bool (Bool "not" (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v1_msualg_1 :::"strict"::: ) ) ")" )))) and (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) and (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F5 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) and (Bool "for" (Set (Var "S")) "," (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set F5 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1"))))))) proof end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "A")) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S"))) ; func :::"MSAlg"::: "(" "A" "," "S" ")" -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" means :: CIRCCMB2:def 1 (Bool it ($#r1_hidden :::"="::: ) "A"); end; :: deftheorem defines :::"MSAlg"::: CIRCCMB2:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_circcmb2 :::"MSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "S")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))); scheme :: CIRCCMB2:sch 20 CIRCCMB29sch20{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~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"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6() -> ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F8() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "A")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F2 "(" ")" )(Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "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 "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))))) ")" ) ")" ))) provided (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))) ")" ) ")" )) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F4 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )))) proof end; scheme :: CIRCCMB2:sch 21 CIRCCMB29sch21{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F4() -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F8() -> ($#m1_hidden :::"Nat":::) } : (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F2 "(" ")" ) "st" (Bool (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F8 "(" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" )))) ")" ) ")" ))) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) provided (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F6 "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F5 "(" (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "n")) ")" )))))) proof end; begin theorem :: CIRCCMB2:9 (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 "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "C1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "C2"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "C2"))))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))))))))) ; theorem :: CIRCCMB2:10 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "C1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "C2"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "C2"))))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))))))))) ; theorem :: CIRCCMB2:11 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#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 "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "C1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "C2"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "C2"))))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool (Set (Var "s2")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set (Var "s")) "is" ($#v1_circuit2 :::"stable"::: ) )))))))) ; theorem :: CIRCCMB2:12 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "C1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "C2"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "C2"))))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool (Set (Var "s2")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set (Var "s")) "is" ($#v1_circuit2 :::"stable"::: ) )))))))) ; theorem :: CIRCCMB2:13 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" ))))))))) ; theorem :: CIRCCMB2:14 (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_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (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 "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" ))))))))) ; theorem :: CIRCCMB2:15 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2"))))))))))) ; theorem :: CIRCCMB2:16 (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 "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s2")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set (Var "s")) "is" ($#v1_circuit2 :::"stable"::: ) )))))))) ; theorem :: CIRCCMB2:17 (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")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_circuit2 :::"stable"::: ) )) "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")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool (Set (Var "s2")) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" ) ")" )))))) ; theorem :: CIRCCMB2:18 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r1_hidden :::"="::: ) (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" )))))))))) ; theorem :: CIRCCMB2:19 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n1")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n1")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n2")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "n1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n2")) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))))))))) ; theorem :: CIRCCMB2:20 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2"))))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A1")) ($#r2_circcomb :::"tolerates"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n1")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n2")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "n1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n2")) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))))))) ; theorem :: CIRCCMB2:21 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (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")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ))))))))))) ; theorem :: CIRCCMB2:22 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (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 "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n1")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) & (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n2")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))))))))) ; theorem :: CIRCCMB2:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (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 "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) & (Bool "(" "not" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) "or" "not" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" )) "holds" (Bool "not" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))))))))) ; theorem :: CIRCCMB2:24 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (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 "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A1")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n1")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A2")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n2")) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))))))) ; scheme :: CIRCCMB2:sch 22 CIRCCMB29sch22{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F3() -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F1 "(" ")" ), F4() -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F7() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F8() -> ($#m1_hidden :::"set"::: ) , F9( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F10( ($#m1_hidden :::"Nat":::)) -> ($#m1_hidden :::"Nat":::) } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F4 "(" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Set F10 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set F10 "(" (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set F10 "(" (Num 1) ")" ) ")" ) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set F6 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )))) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set F3 "(" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set F10 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set F10 "(" (Num 1) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))))) and (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set F10 "(" (Num 2) ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set F10 "(" (Num 2) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F8 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "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 "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_circcomb :::"+*"::: ) (Set (Var "A2")))) & (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) ")" ))))) ")" ) ")" )) and (Bool "(" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" ")" )) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F1 "(" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" ) and (Bool "(" (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F8 "(" ")" )) & (Bool (Set F8 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F1 "(" ")" ))) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) "is" ($#m1_hidden :::"Relation":::)))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set F7 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) & (Bool (Set F9 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))) ")" ))) proof end;