:: MSAFREE1 semantic presentation begin theorem :: MSAFREE1:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "f"))))) ; scheme :: MSAFREE1:sch 1 DTConstrUniq{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lang1 :::"DTConstrStr"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F6() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) } : (Bool (Set F5 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F6 "(" ")" )) provided (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lang1 :::"Terminals"::: ) (Set F1 "(" ")" )))) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "t")) ")" ))) and (Bool "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) ($#k13_finseq_1 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k14_trees_3 :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F2 "(" ")" ) ($#k13_finseq_1 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "ts"))))) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "nt")) "," (Set (Var "ts")) "," (Set (Var "x")) ")" ))))) and (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lang1 :::"Terminals"::: ) (Set F1 "(" ")" )))) "holds" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "t")) ")" ))) and (Bool "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) ($#k13_finseq_1 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k14_trees_3 :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F2 "(" ")" ) ($#k13_finseq_1 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F6 "(" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "ts"))))) "holds" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "nt")) "," (Set (Var "ts")) "," (Set (Var "x")) ")" ))))) proof end; theorem :: MSAFREE1:2 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "o")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_msafree :::"REL"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#k13_finseq_1 :::"*"::: ) )) ")" )))) ; theorem :: MSAFREE1:3 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_msafree :::"REL"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" )))) "implies" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "X")) ")" )) ")" ")" ) ")" ) ")" ))))) ; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> ($#v1_prob_2 :::"disjoint_valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_prob_2 :::"disjoint_valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "D" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "X")) "," (Set (Const "D")); func :::"Flatten"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_card_3 :::"Union"::: ) "X" ")" ) "," (Set "(" ($#k3_card_3 :::"Union"::: ) "D" ")" ) means :: MSAFREE1:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k1_msualg_3 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))); end; :: deftheorem defines :::"Flatten"::: MSAFREE1:def 1 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "X")) "," (Set (Var "D")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_card_3 :::"Union"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_card_3 :::"Union"::: ) (Set (Var "D")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_msafree1 :::"Flatten"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ")" )))))); theorem :: MSAFREE1:4 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "X")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_msafree1 :::"Flatten"::: ) (Set (Var "F1"))) ($#r2_funct_2 :::"="::: ) (Set ($#k1_msafree1 :::"Flatten"::: ) (Set (Var "F2"))))) "holds" (Bool (Set (Var "F1")) ($#r8_pboole :::"="::: ) (Set (Var "F2"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "A" is :::"disjoint_valued"::: means :: MSAFREE1:def 2 (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") "is" ($#v1_prob_2 :::"disjoint_valued"::: ) ); end; :: deftheorem defines :::"disjoint_valued"::: MSAFREE1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_msafree1 :::"disjoint_valued"::: ) ) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) ) ")" ))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"SingleAlg"::: "S" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" means :: MSAFREE1:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ))); end; :: deftheorem defines :::"SingleAlg"::: MSAFREE1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree1 :::"SingleAlg"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ))) ")" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v1_msafree1 :::"disjoint_valued"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k2_msafree1 :::"SingleAlg"::: ) "S") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v1_msafree1 :::"disjoint_valued"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v1_msafree1 :::"disjoint_valued"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") -> ($#v1_prob_2 :::"disjoint_valued"::: ) ; end; theorem :: MSAFREE1:5 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v1_msafree1 :::"disjoint_valued"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A1")) ")" ) "holds" (Bool (Set (Set "(" ($#k1_msafree1 :::"Flatten"::: ) (Set (Var "f")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "a")))))))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k8_msafree :::"FreeSort"::: ) "X") -> ($#v1_prob_2 :::"disjoint_valued"::: ) ; end; scheme :: MSAFREE1:sch 2 FreeSortUniq{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), F3() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set F3 "(" ")" )), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set F3 "(" ")" )), F6() -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k8_msafree :::"FreeSort"::: ) (Set F2 "(" ")" )) "," (Set F3 "(" ")" ), F7() -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k8_msafree :::"FreeSort"::: ) (Set F2 "(" ")" )) "," (Set F3 "(" ")" ) } : (Bool (Set F6 "(" ")" ) ($#r8_pboole :::"="::: ) (Set F7 "(" ")" )) provided (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" ) ")" ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k3_card_3 :::"Union"::: ) (Set F3 "(" ")" ) ")" ) ($#k13_finseq_1 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msafree1 :::"Flatten"::: ) (Set F6 "(" ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "ts"))))) "holds" (Bool (Set (Set "(" (Set F6 "(" ")" ) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "o")) "," (Set (Var "ts")) "," (Set (Var "x")) ")" ))))) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set F2 "(" ")" ) ")" ))) "holds" (Bool (Set (Set "(" (Set F6 "(" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "y")) ")" )))) and (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" ) ")" ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k3_card_3 :::"Union"::: ) (Set F3 "(" ")" ) ")" ) ($#k13_finseq_1 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msafree1 :::"Flatten"::: ) (Set F7 "(" ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "ts"))))) "holds" (Bool (Set (Set "(" (Set F7 "(" ")" ) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "o")) "," (Set (Var "ts")) "," (Set (Var "x")) ")" ))))) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set F2 "(" ")" ) ")" ))) "holds" (Bool (Set (Set "(" (Set F7 "(" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "y")) ")" )))) proof end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k11_msafree :::"FreeMSA"::: ) "X") -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o" "," "A" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k4_msualg_1 :::"Result"::: ) "(" "o" "," "A" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" )) -> ($#v1_prob_2 :::"disjoint_valued"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k11_msafree :::"FreeMSA"::: ) "X") -> ($#v1_msafree1 :::"disjoint_valued"::: ) ; end; scheme :: MSAFREE1:sch 3 ExtFreeGen{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), F3() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4() -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" ) ")" ) "," (Set F3 "(" ")" ), F5() -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" ) ")" ) "," (Set F3 "(" ")" ) } : (Bool (Set F4 "(" ")" ) ($#r8_pboole :::"="::: ) (Set F5 "(" ")" )) provided (Bool (Set F4 "(" ")" ) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" )) "," (Set F3 "(" ")" )) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set F2 "(" ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set F4 "(" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "iff" (Bool P1[(Set (Var "s")) "," (Set (Var "x")) "," (Set (Var "y"))]) ")" ))) and (Bool (Set F5 "(" ")" ) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set F2 "(" ")" )) "," (Set F3 "(" ")" )) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set F2 "(" ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set F5 "(" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "iff" (Bool P1[(Set (Var "s")) "," (Set (Var "x")) "," (Set (Var "y"))]) ")" ))) proof end;