:: MSAFREE3 semantic presentation begin registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#~v1_catalg_1 "non" ($#v1_catalg_1 :::"empty"::: ) ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")) -> ($#~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 "A" be ($#~v1_catalg_1 "non" ($#v1_catalg_1 :::"empty"::: ) ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); mode Element of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")); end; theorem :: MSAFREE3:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_equation :::""""::: ) (Set "(" (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "A")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "A")))))) ; definitionlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); func :::"Free"::: "(" "S" "," "X" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" means :: MSAFREE3:def 1 (Bool "ex" (Set (Var "A")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "(" "X" ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k15_msafree :::"Reverse"::: ) (Set "(" "X" ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ) ($#k1_equation :::""""::: ) "X")) ")" )); end; :: deftheorem defines :::"Free"::: MSAFREE3:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k15_msafree :::"Reverse"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ) ($#k1_equation :::""""::: ) (Set (Var "X")))) ")" )) ")" )))); theorem :: MSAFREE3:2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" ($#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 "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "X")) ")" ))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" ))))) ; theorem :: MSAFREE3:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#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 "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" ) "iff" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" ($#k15_msafree :::"Reverse"::: ) (Set (Var "Y")) ")" ) ($#k1_equation :::""""::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" )))))) ; theorem :: MSAFREE3:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" ($#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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))))))) ; theorem :: MSAFREE3:5 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" )))))) ; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "X" be bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k1_msafree3 :::"Free"::: ) "(" "S" "," "X" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#~v1_catalg_1 "non" ($#v1_catalg_1 :::"empty"::: ) ) ; end; theorem :: MSAFREE3:6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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 "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X"))) ")" )))) ; theorem :: MSAFREE3:7 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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 "x")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ))))) ; theorem :: MSAFREE3:8 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" ) "holds" (Bool (Set (Var "x")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ))))) ; 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 bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" "S" "," "X" ")" ")" ))); 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 bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster -> ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" "S" "," "X" ")" ")" ))); 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 bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster -> ($#v3_trees_9 :::"finite-branching"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" "S" "," "X" ")" ")" ))); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "t" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::); func "S" :::"variables_in"::: "t" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") means :: MSAFREE3:def 2 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_xtuple_0 :::"rng"::: ) "t") : (Bool (Set (Set (Var "a")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" )); end; :: deftheorem defines :::"variables_in"::: MSAFREE3:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "t")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::) (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 (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t"))) : (Bool (Set (Set (Var "a")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" )) ")" )))); definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "t" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::); func "X" :::"variables_in"::: "t" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "X" equals :: MSAFREE3:def 3 (Set "X" ($#k3_pboole :::"/\"::: ) (Set "(" "S" ($#k2_msafree3 :::"variables_in"::: ) "t" ")" )); end; :: deftheorem defines :::"variables_in"::: MSAFREE3:def 3 : (Bool "for" (Set (Var "S")) "being" ($#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" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t")) ")" )))))); theorem :: MSAFREE3:9 (Bool "for" (Set (Var "S")) "being" ($#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" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "V")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set (Var "t")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set "(" (Set (Var "a")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t"))) : (Bool (Set (Set (Var "a")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" ))) ")" ))))) ; theorem :: MSAFREE3:10 (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "implies" (Bool (Set (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" & (Bool "(" "for" (Set (Var "s9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "s9")) ($#r1_hidden :::"<>"::: ) (Set (Var "s"))) "or" "not" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s9"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; theorem :: MSAFREE3:11 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" )) ")" ))))) ; theorem :: MSAFREE3:12 (Bool "for" (Set (Var "S")) "being" ($#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 "s")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "implies" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" & (Bool "(" "for" (Set (Var "s9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "s9")) ($#r1_hidden :::"<>"::: ) (Set (Var "s"))) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s9"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )))) ; theorem :: MSAFREE3:13 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#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 "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set (Var "t")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" )) ")" )))))) ; theorem :: MSAFREE3:14 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) "holds" (Bool (Set (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) (Set (Var "X")))))) ; definitionlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "t" be ($#m1_dtconstr :::"Term":::) "of" (Set (Const "S")) "," (Set (Const "X")); func :::"variables_in"::: "t" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "X" equals :: MSAFREE3:def 4 (Set "S" ($#k2_msafree3 :::"variables_in"::: ) "t"); end; :: deftheorem defines :::"variables_in"::: MSAFREE3:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) "holds" (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t"))))))); theorem :: MSAFREE3:15 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) "holds" (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "X")) ($#k3_msafree3 :::"variables_in"::: ) (Set (Var "t"))))))) ; definitionlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "Y" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); func "S" :::"-Terms"::: "(" "X" "," "Y" ")" -> ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "Y" ")" ) means :: MSAFREE3:def 5 (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 (Var "t")) where t "is" ($#m1_dtconstr :::"Term":::) "of" "S" "," "Y" : (Bool "(" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) "X") ")" ) "}" )); end; :: deftheorem defines :::"-Terms"::: MSAFREE3:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "b4")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "Y")) : (Bool "(" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) ")" ) "}" )) ")" ))))); theorem :: MSAFREE3:16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "x")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "Y")))))))) ; theorem :: MSAFREE3:17 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "Y")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool "(" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) ")" )))))) ; theorem :: MSAFREE3:18 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#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 "(" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" ) ")" )))))) ; theorem :: MSAFREE3:19 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (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 "p")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "Y")) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ))) "iff" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ))) ")" )))))) ; theorem :: MSAFREE3:20 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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 "A")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ))))) ")" )))) ; theorem :: MSAFREE3:21 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is" ($#v3_msualg_2 :::"opers_closed"::: ) )))) ; theorem :: MSAFREE3:22 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set (Set "(" ($#k15_msafree :::"Reverse"::: ) (Set (Var "Y")) ")" ) ($#k1_equation :::""""::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))))) ; theorem :: MSAFREE3:23 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))))))) ; theorem :: MSAFREE3:24 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" )) ($#r8_pboole :::"="::: ) (Set (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" )))) ; theorem :: MSAFREE3:25 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ) ($#k10_msualg_2 :::"|"::: ) (Set "(" (Set (Var "S")) ($#k5_msafree3 :::"-Terms"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" )))) ; theorem :: MSAFREE3:26 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "B")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "Y"))) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B"))))) "holds" (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B"))) "#)" )))))) ; theorem :: MSAFREE3:27 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" ) "holds" (Bool (Set (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))))))) ; theorem :: MSAFREE3:28 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) "holds" (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) (Set (Var "X")))))) ; theorem :: MSAFREE3:29 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "t1")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) (Bool "for" (Set (Var "t2")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "t1")) ($#r1_hidden :::"="::: ) (Set (Var "t2")))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t2")))))))) ; theorem :: MSAFREE3:30 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t"))) ($#r2_pboole :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "t")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")))))) ; theorem :: MSAFREE3:31 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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 ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")))))) ; theorem :: MSAFREE3:32 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "Y")) "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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "Y")) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t"))) "holds" (Bool (Set ($#k4_msafree3 :::"variables_in"::: ) (Set "(" (Set (Var "t")) ($#k8_msaterm :::"|"::: ) (Set (Var "p")) ")" )) ($#r2_pboole :::"c="::: ) (Set ($#k4_msafree3 :::"variables_in"::: ) (Set (Var "t")))))))) ; theorem :: MSAFREE3:33 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" bbbadV3_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 :::"Element":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t"))) "holds" (Bool (Set (Set (Var "t")) ($#k5_trees_2 :::"|"::: ) (Set (Var "p"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" )))))) ; theorem :: MSAFREE3:34 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "t"))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "a")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: MSAFREE3:35 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" bbbadV3_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 :::"Element":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "implies" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t")))) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t"))))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k2_msafree3 :::"variables_in"::: ) (Set (Var "t")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" ) ")" ")" )))))) ; theorem :: MSAFREE3:36 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ")" )) "holds" (Bool (Set ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ))) ; theorem :: MSAFREE3:37 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" )))))) ; theorem :: MSAFREE3:38 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "A")) "being" ($#v1_msualg_6 :::"feasible"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "B")) "is" ($#v1_msualg_6 :::"feasible"::: ) )))) ; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "A" be ($#v1_msualg_6 :::"feasible"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster -> ($#v1_msualg_6 :::"feasible"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "A"; end; theorem :: MSAFREE3:39 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool "(" (Bool (Set ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ) "is" ($#v1_msualg_6 :::"feasible"::: ) ) & (Bool (Set ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "S")) "," (Set (Var "X")) ")" ) "is" ($#v2_msafree :::"free"::: ) ) ")" ))) ; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k1_msafree3 :::"Free"::: ) "(" "S" "," "X" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v2_msafree :::"free"::: ) ($#v1_msualg_6 :::"feasible"::: ) ; end;