:: MSAFREE2 semantic presentation begin definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode Vertex of "S" is ($#m1_subset_1 :::"Element":::) "of" "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"SortsWithConstants"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" "S" equals :: MSAFREE2:def 1 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" : (Bool (Set (Var "v")) "is" ($#v1_msualg_2 :::"with_const_op"::: ) ) "}" if (Bool (Bool "not" "S" "is" ($#v11_struct_0 :::"void"::: ) )) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"SortsWithConstants"::: MSAFREE2:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "S")) "is" ($#v11_struct_0 :::"void"::: ) ))) "implies" (Bool (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) : (Bool (Set (Var "v")) "is" ($#v1_msualg_2 :::"with_const_op"::: ) ) "}" ) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v11_struct_0 :::"void"::: ) )) "implies" (Bool (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"InputVertices"::: "G" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: MSAFREE2:def 2 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "G") ")" )); func :::"InnerVertices"::: "G" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: MSAFREE2:def 3 (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "G")); end; :: deftheorem defines :::"InputVertices"::: MSAFREE2:def 2 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "G"))) ")" )))); :: deftheorem defines :::"InnerVertices"::: MSAFREE2:def 3 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "G")))))); theorem :: MSAFREE2:1 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_struct_0 :::"void"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))))) ; theorem :: MSAFREE2:2 (Bool "for" (Set (Var "G")) "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_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G"))))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ; theorem :: MSAFREE2:3 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "G"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "G"))))) ; theorem :: MSAFREE2:4 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "G"))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "IT" is :::"with_input_V"::: means :: MSAFREE2:def 4 (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) "IT") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"with_input_V"::: MSAFREE2:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_msafree2 :::"with_input_V"::: ) ) "iff" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IT"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msafree2 :::"with_input_V"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msafree2 :::"with_input_V"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k2_msafree2 :::"InputVertices"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k3_msafree2 :::"InnerVertices"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "MSA" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); mode :::"InputValues"::: "of" "MSA" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_msafree2 :::"InputVertices"::: ) "S") means :: MSAFREE2:def 5 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "S" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) "S"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MSA") ($#k1_funct_1 :::"."::: ) (Set (Var "v"))))); end; :: deftheorem defines :::"InputValues"::: MSAFREE2:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "MSA")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "MSA"))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MSA"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))))) ")" )))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "S" is :::"Circuit-like"::: means :: MSAFREE2:def 6 (Bool "for" (Set (Var "S9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S9")) ($#r1_hidden :::"="::: ) "S")) "holds" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S9")) "st" (Bool (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "o2"))))); end; :: deftheorem defines :::"Circuit-like"::: MSAFREE2:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_msafree2 :::"Circuit-like"::: ) ) "iff" (Bool "for" (Set (Var "S9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S9")) ($#r1_hidden :::"="::: ) (Set (Var "S")))) "holds" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S9")) "st" (Bool (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "o2"))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_struct_0 :::"void"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msualg_1 :::"strict"::: ) ($#v2_msafree2 :::"Circuit-like"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "IIG")); assume (Bool (Set (Const "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Const "IIG")))) ; func :::"action_at"::: "v" -> ($#m1_subset_1 :::"OperSymbol":::) "of" "IIG" means :: MSAFREE2:def 7 (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) it) ($#r1_hidden :::"="::: ) "v"); end; :: deftheorem defines :::"action_at"::: MSAFREE2:def 7 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "IIG")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")))) "iff" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))); begin theorem :: MSAFREE2: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (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 "MSA" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func :::"FreeEnv"::: "MSA" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" equals :: MSAFREE2:def 8 (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MSA")); end; :: deftheorem defines :::"FreeEnv"::: MSAFREE2: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 "MSA")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "MSA"))) ($#r1_hidden :::"="::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MSA"))))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "MSA" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func :::"Eval"::: "MSA" -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "MSA" ")" ) "," "MSA" means :: MSAFREE2:def 9 (Bool "(" (Bool it ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k5_msafree2 :::"FreeEnv"::: ) "MSA") "," "MSA") & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MSA") "," (Set (Var "s")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MSA") ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set "(" it ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ) ")" ); end; :: deftheorem defines :::"Eval"::: MSAFREE2: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 "MSA")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "MSA")) ")" ) "," (Set (Var "MSA")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_msafree2 :::"Eval"::: ) (Set (Var "MSA")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "MSA"))) "," (Set (Var "MSA"))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k7_msafree :::"FreeSort"::: ) "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MSA"))) "," (Set (Var "s")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MSA"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set "(" (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ) ")" ) ")" )))); theorem :: MSAFREE2: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "is" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "A"))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "IT" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "IT" is :::"finitely-generated"::: means :: MSAFREE2:def 10 (Bool "for" (Set (Var "S9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S9")) ($#r1_hidden :::"="::: ) "S")) "holds" (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S9")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "IT")) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "G")) "is" bbbadV2_FINSET_1())))) if (Bool (Bool "not" "S" "is" ($#v11_struct_0 :::"void"::: ) )) otherwise (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "IT") "is" bbbadV2_FINSET_1()); end; :: deftheorem defines :::"finitely-generated"::: MSAFREE2:def 10 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "S")) "is" ($#v11_struct_0 :::"void"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_msafree2 :::"finitely-generated"::: ) ) "iff" (Bool "for" (Set (Var "S9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S9")) ($#r1_hidden :::"="::: ) (Set (Var "S")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S9")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "IT")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "G")) "is" bbbadV2_FINSET_1())))) ")" ) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v11_struct_0 :::"void"::: ) )) "implies" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_msafree2 :::"finitely-generated"::: ) ) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "IT"))) "is" bbbadV2_FINSET_1()) ")" ) ")" ")" ))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "IT" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "IT" is :::"finite-yielding"::: means :: MSAFREE2:def 11 (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "IT") "is" bbbadV2_FINSET_1()); end; :: deftheorem defines :::"finite-yielding"::: MSAFREE2:def 11 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_msafree2 :::"finite-yielding"::: ) ) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "IT"))) "is" bbbadV2_FINSET_1()) ")" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) -> ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"Trivial_Algebra"::: "S" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" means :: MSAFREE2:def 12 (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))); end; :: deftheorem defines :::"Trivial_Algebra"::: MSAFREE2:def 12 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_msafree2 :::"Trivial_Algebra"::: ) (Set (Var "S")))) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b2"))) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) ")" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "IT" is :::"monotonic"::: means :: MSAFREE2:def 13 (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "IT" "holds" (Bool (Set (Var "A")) "is" ($#v4_msafree2 :::"finite-yielding"::: ) )); end; :: deftheorem defines :::"monotonic"::: MSAFREE2:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_msafree2 :::"monotonic"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IT")) "holds" (Bool (Set (Var "A")) "is" ($#v4_msafree2 :::"finite-yielding"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; theorem :: MSAFREE2:7 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "holds" (Bool (Set (Var "e")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::)))))) ; theorem :: MSAFREE2:8 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) "is" ($#v3_msafree2 :::"finitely-generated"::: ) ))) ; theorem :: MSAFREE2: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" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S"))))) "holds" (Bool "ex" (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 "v"))) "st" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )))))))) ; theorem :: MSAFREE2:10 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (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 "p"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))))))) ; theorem :: MSAFREE2:11 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (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 "p"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) "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 "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) "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 "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) "v"); end; registrationlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "IIG"))); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "IIG")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) "v"); end; theorem :: MSAFREE2:12 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Set (Var "e")) ($#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 "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "v" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Const "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Const "v"))); func :::"depth"::: "e" -> ($#m1_hidden :::"Nat":::) means :: MSAFREE2:def 14 (Bool "ex" (Set (Var "dt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::)(Bool "ex" (Set (Var "t")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool "(" (Bool (Set (Var "dt")) ($#r1_hidden :::"="::: ) "e") & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "dt")))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "t")))) ")" ))); end; :: deftheorem defines :::"depth"::: MSAFREE2:def 14 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_msafree2 :::"depth"::: ) (Set (Var "e")))) "iff" (Bool "ex" (Set (Var "dt")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::)(Bool "ex" (Set (Var "t")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool "(" (Bool (Set (Var "dt")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "dt")))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "t")))) ")" ))) ")" ))))));