:: MSAFREE semantic presentation begin theorem :: MSAFREE:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "(" (Set (Var "J")) ($#k3_finseq_2 :::"*"::: ) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "J")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")) ")" ))))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "C" be ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Const "A")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); func "F" :::"||"::: "C" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "C" "," "B" means :: MSAFREE:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" "C" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))); end; :: deftheorem defines :::"||"::: MSAFREE:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "C")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "b6")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))) ")" )))))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I"))) ; func :::"coprod"::: "(" "i" "," "X" ")" -> ($#m1_hidden :::"set"::: ) means :: MSAFREE:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) "i")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," "i" ($#k4_tarski :::"]"::: ) )) ")" )) ")" )); end; :: deftheorem defines :::"coprod"::: MSAFREE:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set (Var "i")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) )) ")" )) ")" )) ")" ))))); notationlet "I" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); synonym :::"coprod"::: "X" for :::"disjoin"::: "I"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k2_card_3 :::"coprod"::: ) ) -> "I" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k2_card_3 :::"coprod"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"coprod"::: redefine func :::"coprod"::: "X" -> ($#m1_hidden :::"set"::: ) means :: MSAFREE:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "I") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set (Var "i")) "," "X" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"coprod"::: MSAFREE:def 3 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_msafree :::"coprod"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set (Var "i")) "," (Set (Var "X")) ")" )) ")" ) ")" ) ")" )))); registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k2_card_3 :::"coprod"::: ) ) -> bbbadV2_RELAT_1() ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k3_card_3 :::"Union"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MSAFREE:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U0" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); mode :::"GeneratorSet"::: "of" "U0" -> ($#m3_pboole :::"MSSubset":::) "of" "U0" means :: MSAFREE:def 4 (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k12_msualg_2 :::"GenMSAlg"::: ) it ")" )) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U0")); end; :: deftheorem defines :::"GeneratorSet"::: MSAFREE:def 4 : (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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "U0"))) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "b3")) ")" )) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0")))) ")" )))); theorem :: MSAFREE: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 "U0")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "U0"))) "iff" (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "U0"))) ")" )))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U0" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "IT" be ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Const "U0")); attr "IT" is :::"free"::: means :: MSAFREE:def 5 (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" "IT" "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) (Bool "ex" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" "U0" "," (Set (Var "U1")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) "U0" "," (Set (Var "U1"))) & (Bool (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) "IT") ($#r8_pboole :::"="::: ) (Set (Var "f"))) ")" )))); end; :: deftheorem defines :::"free"::: MSAFREE:def 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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "IT")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_msafree :::"free"::: ) ) "iff" (Bool "for" (Set (Var "U1")) "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 "IT")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) (Bool "ex" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U0")) "," (Set (Var "U1")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U0")) "," (Set (Var "U1"))) & (Bool (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) (Set (Var "IT"))) ($#r8_pboole :::"="::: ) (Set (Var "f"))) ")" )))) ")" )))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "IT" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "IT" is :::"free"::: means :: MSAFREE:def 6 (Bool "ex" (Set (Var "G")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" "IT" "st" (Bool (Set (Var "G")) "is" ($#v1_msafree :::"free"::: ) )); end; :: deftheorem defines :::"free"::: MSAFREE:def 6 : (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 "IT")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_msafree :::"free"::: ) ) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "IT")) "st" (Bool (Set (Var "G")) "is" ($#v1_msafree :::"free"::: ) )) ")" ))); theorem :: MSAFREE:4 (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"))) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" )) ($#r1_xboole_0 :::"misses"::: ) (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 :::":]"::: ) )))) ; begin definitionlet "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 ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); func :::"REL"::: "X" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) means :: MSAFREE:def 7 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" )) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "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" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "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"::: ) "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")) ")" ) "," "X" ")" )) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"REL"::: MSAFREE:def 7 : (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 "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (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")) ")" ) ")" ) ")" ) "," (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")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_msafree :::"REL"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (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")) ")" ) ")" )) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (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")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#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 "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "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")) ")" )) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))) ")" )))); theorem :: MSAFREE: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 "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" ($#m2_finseq_2 :::"Element"::: ) "of" (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")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (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")))) "iff" (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")) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))) ; definitionlet "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 ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); func :::"DTConMSA"::: "X" -> ($#l1_lang1 :::"DTConstrStr"::: ) equals :: MSAFREE:def 8 (Set ($#g1_lang1 :::"DTConstrStr"::: ) "(#" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) "," (Set "(" ($#k4_msafree :::"REL"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"DTConMSA"::: MSAFREE:def 8 : (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"))) "holds" (Bool (Set ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_lang1 :::"DTConstrStr"::: ) "(#" (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")) ")" ) ")" ) ")" ) "," (Set "(" ($#k4_msafree :::"REL"::: ) (Set (Var "X")) ")" ) "#)" )))); 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 ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k5_msafree :::"DTConMSA"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lang1 :::"strict"::: ) ; end; theorem :: MSAFREE:6 (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"))) "holds" (Bool "(" (Bool (Set ($#k2_lang1 :::"NonTerminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (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 ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_lang1 :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))) & "(" (Bool (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1())) "implies" (Bool "(" (Bool (Set ($#k2_lang1 :::"NonTerminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (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 ($#k1_lang1 :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ))) ")" ) ")" ")" ))) ; 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 ($#k5_msafree :::"DTConMSA"::: ) "X") -> ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ; end; theorem :: MSAFREE:7 (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 "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lang1 :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1())) "implies" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))(Bool "ex" (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 "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (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 "s"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_lang1 :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )))) ")" ) ")" )))) ; definitionlet "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"))); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func :::"Sym"::: "(" "o" "," "X" ")" -> ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "X" ")" ) equals :: MSAFREE:def 9 (Set ($#k4_tarski :::"["::: ) "o" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"Sym"::: MSAFREE:def 9 : (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" bbbadV2_RELAT_1() ($#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")) "holds" (Bool (Set ($#k6_msafree :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))))); definitionlet "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"))); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); func :::"FreeSort"::: "(" "X" "," "s" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "X" ")" ) ")" ) equals :: MSAFREE:def 10 "{" (Set (Var "a")) where a "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "X" ")" )) : (Bool "(" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) "s")) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," "s" ($#k4_tarski :::"]"::: ) ))) ")" )) "or" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) "s") ")" )) ")" ) "}" ; end; :: deftheorem defines :::"FreeSort"::: MSAFREE:def 10 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set (Var "X")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) : (Bool "(" (Bool "ex" (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 "s")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) ")" )) "or" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" )) ")" ) "}" )))); 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"))); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set ($#k7_msafree :::"FreeSort"::: ) "(" "X" "," "s" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "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"))); func :::"FreeSort"::: "X" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") means :: MSAFREE:def 11 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" "X" "," (Set (Var "s")) ")" ))); end; :: deftheorem defines :::"FreeSort"::: MSAFREE:def 11 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set (Var "X")) "," (Set (Var "s")) ")" ))) ")" )))); 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") -> bbbadV2_RELAT_1() ; end; theorem :: MSAFREE:8 (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" bbbadV2_RELAT_1() ($#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 "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set (Var "x")) "is" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))))))) ; theorem :: MSAFREE:9 (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" bbbadV2_RELAT_1() ($#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 "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set (Var "X")) "," (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" ) ")" ))))) ; theorem :: MSAFREE:10 (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" bbbadV2_RELAT_1() ($#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 "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_msafree :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) ")" ))))) ; theorem :: MSAFREE:11 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))))) ; theorem :: MSAFREE:12 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"<>"::: ) (Set (Var "s2")))) "holds" (Bool (Set (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_subset_1 :::"misses"::: ) (Set (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))))) ; definitionlet "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"))); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func :::"DenOp"::: "(" "o" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) "X" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S") ")" ) ($#k1_funct_1 :::"."::: ) "o" ")" ) "," (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) "X" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S") ")" ) ($#k1_funct_1 :::"."::: ) "o" ")" ) means :: MSAFREE:def 12 (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "X" ")" )) "st" (Bool (Bool (Set ($#k6_msafree :::"Sym"::: ) "(" "o" "," "X" ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_msafree :::"Sym"::: ) "(" "o" "," "X" ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p"))))); end; :: deftheorem defines :::"DenOp"::: MSAFREE:def 12 : (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" bbbadV2_RELAT_1() ($#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 "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_msafree :::"DenOp"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set ($#k6_msafree :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_msafree :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p"))))) ")" ))))); definitionlet "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"))); func :::"FreeOper"::: "X" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) "X" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S")) "," (Set (Set "(" ($#k8_msafree :::"FreeSort"::: ) "X" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S")) means :: MSAFREE:def 13 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "o"))) ($#r6_pboole :::"="::: ) (Set ($#k9_msafree :::"DenOp"::: ) "(" (Set (Var "o")) "," "X" ")" ))); end; :: deftheorem defines :::"FreeOper"::: MSAFREE:def 13 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S")))) "," (Set (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_msafree :::"FreeOper"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set (Var "o"))) ($#r6_pboole :::"="::: ) (Set ($#k9_msafree :::"DenOp"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ))) ")" )))); definitionlet "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"))); func :::"FreeMSA"::: "X" -> ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" equals :: MSAFREE:def 14 (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "(" ($#k8_msafree :::"FreeSort"::: ) "X" ")" ) "," (Set "(" ($#k10_msafree :::"FreeOper"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"FreeMSA"::: MSAFREE:def 14 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_msafree :::"FreeOper"::: ) (Set (Var "X")) ")" ) "#)" )))); 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") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ; end; definitionlet "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"))); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); func :::"FreeGen"::: "(" "s" "," "X" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) "X" ")" ) ($#k1_funct_1 :::"."::: ) "s" ")" ) means :: MSAFREE:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) "s")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," "s" ($#k4_tarski :::"]"::: ) ))) ")" )) ")" )); end; :: deftheorem defines :::"FreeGen"::: MSAFREE:def 15 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) ")" )) ")" )) ")" ))))); 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"))); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set ($#k12_msafree :::"FreeGen"::: ) "(" "s" "," "X" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MSAFREE:13 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ) : (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "t")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ) "}" )))) ; definitionlet "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"))); func :::"FreeGen"::: "X" -> ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set ($#k11_msafree :::"FreeMSA"::: ) "X") means :: MSAFREE:def 16 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," "X" ")" ))); end; :: deftheorem defines :::"FreeGen"::: MSAFREE:def 16 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) ")" )))); theorem :: MSAFREE:14 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X"))) "is" bbbadV2_RELAT_1()))) ; theorem :: MSAFREE:15 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ) : (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))) "}" ))) ; definitionlet "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"))); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); func :::"Reverse"::: "(" "s" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" "s" "," "X" ")" ")" ) "," (Set "(" "X" ($#k1_funct_1 :::"."::: ) "s" ")" ) means :: MSAFREE:def 17 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "X" ")" ) "st" (Bool (Bool (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" "s" "," "X" ")" ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_xtuple_0 :::"`1"::: ) ))); end; :: deftheorem defines :::"Reverse"::: MSAFREE:def 17 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k14_msafree :::"Reverse"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_xtuple_0 :::"`1"::: ) ))) ")" ))))); definitionlet "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"))); func :::"Reverse"::: "X" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k13_msafree :::"FreeGen"::: ) "X") "," "X" means :: MSAFREE:def 18 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "holds" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "s"))) ($#r1_funct_2 :::"="::: ) (Set ($#k14_msafree :::"Reverse"::: ) "(" (Set (Var "s")) "," "X" ")" ))); end; :: deftheorem defines :::"Reverse"::: MSAFREE:def 18 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X"))) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_msafree :::"Reverse"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s"))) ($#r1_funct_2 :::"="::: ) (Set ($#k14_msafree :::"Reverse"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) ")" )))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X", "A" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k13_msafree :::"FreeGen"::: ) (Set (Const "X"))) "," (Set (Const "A")); let "t" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Const "X")) ")" ); assume (Bool (Set (Const "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Const "X")) ")" ))) ; func :::"pi"::: "(" "F" "," "A" "," "t" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) "A") means :: MSAFREE:def 19 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" "t" ($#k2_xtuple_0 :::"`2"::: ) ")" )))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) "t" ")" )))); end; :: deftheorem defines :::"pi"::: MSAFREE:def 19 : (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")) "," (Set (Var "A")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X"))) "," (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" )))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k16_msafree :::"pi"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) "," (Set (Var "t")) ")" )) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k2_xtuple_0 :::"`2"::: ) ")" )))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )))) ")" )))))); definitionlet "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"))); let "t" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Const "X")) ")" ); assume (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Const "t")) ($#r1_lang1 :::"==>"::: ) (Set (Var "p")))) ; func :::"@"::: "(" "X" "," "t" ")" -> ($#m1_subset_1 :::"OperSymbol":::) "of" "S" means :: MSAFREE:def 20 (Bool (Set ($#k4_tarski :::"["::: ) it "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) "t"); end; :: deftheorem defines :::"@"::: MSAFREE:def 20 : (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "t")) ($#r1_lang1 :::"==>"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k17_msafree :::"@"::: ) "(" (Set (Var "X")) "," (Set (Var "t")) ")" )) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b4")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "p" be ($#m1_hidden :::"FinSequence":::); assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Const "o")) "," (Set (Const "U0")) ")" )) ; func :::"pi"::: "(" "o" "," "U0" "," "p" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U0")) equals :: MSAFREE:def 21 (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" "o" "," "U0" ")" ")" ) ($#k1_funct_1 :::"."::: ) "p"); end; :: deftheorem defines :::"pi"::: MSAFREE:def 21 : (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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ))) "holds" (Bool (Set ($#k18_msafree :::"pi"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))))))); theorem :: MSAFREE:16 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X"))) "is" ($#v1_msafree :::"free"::: ) ))) ; theorem :: MSAFREE:17 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) "is" ($#v2_msafree :::"free"::: ) ))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; 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 "U0" be ($#v2_msafree :::"free"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_msafree :::"free"::: ) for ($#m1_msafree :::"GeneratorSet"::: ) "of" "U0"; end; theorem :: MSAFREE:18 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "ex" (Set (Var "U0")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S"))(Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U0")) "," (Set (Var "U1")) "st" (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U0")) "," (Set (Var "U1"))))))) ; theorem :: MSAFREE:19 (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 "U1")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "ex" (Set (Var "U0")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S"))(Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U0")) "," (Set (Var "U1")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U0")) "," (Set (Var "U1"))) & (Bool (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) ")" ))))) ;