:: MSATERM semantic presentation 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 "V" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); func "S" :::"-Terms"::: "V" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_trees_3 :::"FinTrees"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "V" ")" )) ")" ) equals :: MSATERM:def 1 (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "V" ")" )); end; :: deftheorem defines :::"-Terms"::: MSATERM:def 1 : (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 "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "V")) ")" ))))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set "S" ($#k1_msaterm :::"-Terms"::: ) "V") -> ($#~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 "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); mode Term of "S" "," "V" is ($#m1_dtconstr :::"Element"::: ) "of" (Set "S" ($#k1_msaterm :::"-Terms"::: ) "V"); 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 "V" 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")); :: original: :::"Sym"::: redefine func :::"Sym"::: "(" "o" "," "V" ")" -> ($#m2_subset_1 :::"NonTerminal":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "V" ")" ); 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 "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "sy" be ($#m2_subset_1 :::"NonTerminal":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Const "V")) ")" ); mode :::"ArgumentSeq"::: "of" "sy" -> ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set "S" ($#k1_msaterm :::"-Terms"::: ) "V") means :: MSATERM:def 2 (Bool it "is" ($#m2_dtconstr :::"SubtreeSeq"::: ) "of" "sy"); end; :: deftheorem defines :::"ArgumentSeq"::: MSATERM:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "sy")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set (Var "sy"))) "iff" (Bool (Set (Var "b4")) "is" ($#m2_dtconstr :::"SubtreeSeq"::: ) "of" (Set (Var "sy"))) ")" ))))); theorem :: MSATERM:1 (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 "V")) "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 "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")))) & (Bool (Set (Var "a")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) ")" ) "iff" (Bool (Set (Var "a")) "is" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" )) ")" ))))) ; scheme :: MSATERM:sch 1 TermInd{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "holds" (Bool P1[(Set (Var "t"))])) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool P1[(Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))]))) and (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set F2 "(" ")" ) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool P1[(Set (Var "t"))]) ")" )) "holds" (Bool P1[(Set (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")))]))) proof 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 ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); mode c-Term of "A" "," "V" is ($#m1_dtconstr :::"Term":::) "of" "S" "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ($#k2_pboole :::"\/"::: ) "V" ")" ); 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 ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" 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")); mode ArgumentSeq of "o" "," "A" "," "V" is ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" "o" "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ($#k2_pboole :::"\/"::: ) "V" ")" ) ")" ); end; scheme :: MSATERM:sch 2 CTermInd{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F3() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "holds" (Bool P1[(Set (Var "t"))])) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set F2 "(" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool P1[(Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))]))) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool P1[(Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))]))) and (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_msaterm :::"ArgumentSeq":::) "of" (Set (Var "o")) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool P1[(Set (Var "t"))]) ")" )) "holds" (Bool P1[(Set (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set F2 "(" ")" )) ($#k2_pboole :::"\/"::: ) (Set F3 "(" ")" ) ")" ) ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p")))]))) proof 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 "V" 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 "V")); let "p" be ($#m1_trees_1 :::"Node":::) "of" (Set (Const "t")); :: original: :::"."::: redefine func "t" :::"."::: "p" -> ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) "V" ")" ); 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 "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "S" ($#k1_msaterm :::"-Terms"::: ) "V"); end; theorem :: MSATERM:2 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "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 "V")) "holds" (Bool "(" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "or" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#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 :::":]"::: ) )) ")" )))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) "holds" (Bool "(" (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 "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ")" ))) "or" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "or" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#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 :::":]"::: ) )) ")" ))))) ; theorem :: MSATERM: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 "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V"))))))) ; theorem :: MSATERM: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 "V")) "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 "V")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (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 "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#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 :::"]"::: ) )) "is" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (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 "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) "is" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))))))))) ; theorem :: MSATERM: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 "V")) "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 "V")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" ) "st" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "a"))))))))) ; 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 ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" 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")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A"))) ($#k1_funct_1 :::"."::: ) (Set (Const "s"))); func "x" :::"-term"::: "(" "A" "," "V" ")" -> ($#m1_dtconstr :::"c-Term":::) "of" "A" "," "V" equals :: MSATERM:def 3 (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) "x" "," "s" ($#k4_tarski :::"]"::: ) )); end; :: deftheorem defines :::"-term"::: MSATERM:def 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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "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_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set (Var "x")) ($#k4_msaterm :::"-term"::: ) "(" (Set (Var "A")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (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 "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" 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")); let "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "V")) ($#k1_funct_1 :::"."::: ) (Set (Const "s"))); func "v" :::"-term"::: "A" -> ($#m1_dtconstr :::"c-Term":::) "of" "A" "," "V" equals :: MSATERM:def 4 (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) "v" "," "s" ($#k4_tarski :::"]"::: ) )); end; :: deftheorem defines :::"-term"::: MSATERM: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set (Var "v")) ($#k5_msaterm :::"-term"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (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 "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "sy" be ($#m2_subset_1 :::"NonTerminal":::) "of" (Set "(" ($#k5_msafree :::"DTConMSA"::: ) (Set (Const "V")) ")" ); let "p" be ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set (Const "sy")); :: original: :::"-tree"::: redefine func "sy" :::"-tree"::: "p" -> ($#m1_dtconstr :::"Term":::) "of" "S" "," "V"; end; scheme :: MSATERM:sch 3 TermInd2{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F3() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "holds" (Bool P1[(Set (Var "t"))])) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set F2 "(" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool P1[(Set (Set (Var "x")) ($#k4_msaterm :::"-term"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" )]))) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool P1[(Set (Set (Var "v")) ($#k5_msaterm :::"-term"::: ) (Set F2 "(" ")" ))]))) and (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set F2 "(" ")" )) ($#k2_pboole :::"\/"::: ) (Set F3 "(" ")" ) ")" ) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool P1[(Set (Var "t"))]) ")" )) "holds" (Bool P1[(Set (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set F2 "(" ")" )) ($#k2_pboole :::"\/"::: ) (Set F3 "(" ")" ) ")" ) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p")))]))) proof end; begin theorem :: MSATERM: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 "V")) "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 "V")) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set (Var "V")) "," (Set (Var "s")) ")" )))))) ; theorem :: MSATERM: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 "V")) "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 "V")) "," (Set (Var "s")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V"))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k8_msafree :::"FreeSort"::: ) (Set (Var "V")) ")" ))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" 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 "V")); func :::"the_sort_of"::: "t" -> ($#m1_subset_1 :::"SortSymbol":::) "of" "S" means :: MSATERM:def 5 (Bool "t" ($#r2_hidden :::"in"::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" "V" "," it ")" )); end; :: deftheorem defines :::"the_sort_of"::: MSATERM: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 "V")) "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 "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t")))) "iff" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set (Var "V")) "," (Set (Var "b4")) ")" )) ")" ))))); theorem :: MSATERM: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 "V")) "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 "V")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s")))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (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 "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))))))))) ; theorem :: MSATERM: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 "V")) "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 "V")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set "(" (Set (Var "x")) ($#k4_msaterm :::"-term"::: ) "(" (Set (Var "A")) "," (Set (Var "V")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s")))))))) ; theorem :: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set "(" (Set (Var "v")) ($#k5_msaterm :::"-term"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s")))))))) ; theorem :: MSATERM: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 "V")) "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_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" ) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set "(" (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")))))))) ; begin theorem :: MSATERM: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 "V")) "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 "a")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" )) "iff" (Bool (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "a")))) ")" ))))) ; theorem :: MSATERM:22 (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 "V")) "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 "a")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V"))) ")" ) ")" ))))) ; theorem :: MSATERM:23 (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 "V")) "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 "a")) "being" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) & (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) ")" ))))))) ; theorem :: MSATERM:24 (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 "V")) "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 "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) "or" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) ")" ) & (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) "or" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) ")" ))) ")" )) "holds" (Bool (Set (Var "a")) "is" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" )))))) ; theorem :: MSATERM:25 (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 "V")) "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 "a")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V"))) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) "or" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) ")" ) & (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) "or" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))))) ")" )) "holds" (Bool (Set (Var "a")) "is" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" )))))) ; theorem :: MSATERM:26 (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 "V1")) "," (Set (Var "V2")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "st" (Bool (Bool (Set (Var "V1")) ($#r2_pboole :::"c="::: ) (Set (Var "V2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V1")) "holds" (Bool (Set (Var "t")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V2")))))) ; theorem :: MSATERM:27 (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 "V")) "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 "V")) "holds" (Bool (Set (Var "t")) "is" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V"))))))) ; 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 "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); mode :::"CompoundTerm"::: "of" "S" "," "V" -> ($#m1_dtconstr :::"Term":::) "of" "S" "," "V" means :: MSATERM:def 6 (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#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 :::":]"::: ) )); end; :: deftheorem defines :::"CompoundTerm"::: MSATERM: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 "V")) "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_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V"))) "iff" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#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 :::":]"::: ) )) ")" )))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); mode :::"SetWithCompoundTerm"::: "of" "S" "," "V" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "S" ($#k1_msaterm :::"-Terms"::: ) "V" ")" ) means :: MSATERM:def 7 (Bool "ex" (Set (Var "t")) "being" ($#m2_msaterm :::"CompoundTerm"::: ) "of" "S" "," "V" "st" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) it)); end; :: deftheorem defines :::"SetWithCompoundTerm"::: MSATERM: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V"))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) ")" )))); theorem :: MSATERM:28 (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 "V")) "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 "V")) "st" (Bool (Bool (Bool "not" (Set (Var "t")) "is" ($#v1_zfmisc_1 :::"root"::: ) ))) "holds" (Bool (Set (Var "t")) "is" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")))))) ; theorem :: MSATERM:29 (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 "V")) "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 "V")) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "holds" (Bool (Set (Set (Var "t")) ($#k5_trees_2 :::"|"::: ) (Set (Var "p"))) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" 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 "V")); let "p" be ($#m1_trees_1 :::"Node":::) "of" (Set (Const "t")); :: original: :::"|"::: redefine func "t" :::"|"::: "p" -> ($#m1_dtconstr :::"Term":::) "of" "S" "," "V"; end; 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 "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); mode :::"Variables"::: "of" "A" -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") means :: MSATERM:def 8 (Bool it ($#r5_pboole :::"misses"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")); end; :: deftheorem defines :::"Variables"::: MSATERM: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set (Var "b3")) ($#r5_pboole :::"misses"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) ")" )))); theorem :: MSATERM:30 (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 "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (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 "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))))))))) ; 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 ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "t" be ($#m1_dtconstr :::"c-Term":::) "of" (Set (Const "A")) "," (Set (Const "V")); let "f" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A"))); let "vt" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::); pred "vt" :::"is_an_evaluation_of"::: "t" "," "f" means :: MSATERM:def 9 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "vt") ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "t")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" "vt" "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set "t" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set "vt" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set "t" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set "vt" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set "t" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set "vt" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," "A" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_9 :::"succ"::: ) "(" "vt" "," (Set (Var "p")) ")" ")" ))) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_an_evaluation_of"::: MSATERM: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "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 :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vt"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "vt")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_9 :::"succ"::: ) "(" (Set (Var "vt")) "," (Set (Var "p")) ")" ")" ))) ")" ) ")" ) ")" ) ")" ) ")" ))))))); theorem :: MSATERM:31 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "x"))) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))))))))) ; theorem :: MSATERM:32 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set ($#k2_trees_4 :::"root-tree"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))))))))) ; theorem :: MSATERM:33 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (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 (Var "o")) "," (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "ex" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "vt")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f"))) ")" ))) ")" )) "holds" (Bool "ex" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "vt")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k14_trees_3 :::"roots"::: ) (Set (Var "q")) ")" ) ")" ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q")))) & (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k2_pboole :::"\/"::: ) (Set (Var "V")) ")" ) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p"))) "," (Set (Var "f"))) ")" ))))))))) ; theorem :: MSATERM:34 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "e")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) (Bool "for" (Set (Var "n")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "e")) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "e")) ($#k5_trees_2 :::"|"::: ) (Set (Var "n"))) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Set (Var "t")) ($#k8_msaterm :::"|"::: ) (Set (Var "p"))) "," (Set (Var "f"))))))))))) ; theorem :: MSATERM:35 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (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 (Var "o")) "," (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k2_pboole :::"\/"::: ) (Set (Var "V")) ")" ) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p"))) "," (Set (Var "f")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "vt")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k14_trees_3 :::"roots"::: ) (Set (Var "q")) ")" ) ")" ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "ex" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "vt")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f"))) ")" ))) ")" ) ")" ))))))))) ; theorem :: MSATERM:36 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "ex" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f"))))))))) ; theorem :: MSATERM: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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "e1")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f"))) & (Bool (Set (Var "e2")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2"))))))))) ; theorem :: MSATERM:38 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))) "holds" (Bool (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_msaterm :::"the_sort_of"::: ) (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 "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" be ($#m4_msaterm :::"Variables"::: ) "of" (Set (Const "A")); let "t" be ($#m1_dtconstr :::"c-Term":::) "of" (Set (Const "A")) "," (Set (Const "V")); let "f" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A"))); func "t" :::"@"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_msaterm :::"the_sort_of"::: ) "t" ")" )) means :: MSATERM:def 10 (Bool "ex" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) "t" "," "f") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )); end; :: deftheorem defines :::"@"::: MSATERM: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k9_msaterm :::"@"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f"))) & (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ")" ))))))); theorem :: MSATERM:39 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))) "holds" (Bool (Set (Set (Var "t")) ($#k9_msaterm :::"@"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))))))) ; theorem :: MSATERM:40 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "vt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "vt")) ($#r1_msaterm :::"is_an_evaluation_of"::: ) (Set (Var "t")) "," (Set (Var "f")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "holds" (Bool (Set (Set (Var "vt")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k8_msaterm :::"|"::: ) (Set (Var "p")) ")" ) ($#k9_msaterm :::"@"::: ) (Set (Var "f"))))))))))) ; theorem :: MSATERM:41 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_msaterm :::"-term"::: ) "(" (Set (Var "A")) "," (Set (Var "V")) ")" ")" ) ($#k9_msaterm :::"@"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))))) ; theorem :: MSATERM:42 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k5_msaterm :::"-term"::: ) (Set (Var "A")) ")" ) ($#k9_msaterm :::"@"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v")))))))))) ; theorem :: MSATERM:43 (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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (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 (Var "o")) "," (Set (Var "A")) "," (Set (Var "V")) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k9_msaterm :::"@"::: ) (Set (Var "f"))))) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k2_pboole :::"\/"::: ) (Set (Var "V")) ")" ) ")" ")" ) ($#k6_msaterm :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k9_msaterm :::"@"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))))))))))) ;