:: MSAFREE2 semantic presentation

begin

definition
let S be ( ( ) ( ) ManySortedSign ) ;
mode Vertex of S is ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
func SortsWithConstants S -> ( ( ) ( ) Subset of ) equals :: MSAFREE2:def 1
 { v : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) where v is ( ( ) ( ) SortSymbol of ( ( ) ( ) set ) ) : v : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) is with_const_op } if not S : ( ( ) ( ) GrammarStr ) is void
otherwise {} : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) ;
end;

definition
let G be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
func InputVertices G -> ( ( ) ( ) Subset of ) equals :: MSAFREE2:def 2
 the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) \ (rng the ResultSort of G : ( ( ) ( ) GrammarStr ) : ( ( Function-like V29( the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) -defined the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) -valued Function-like V29( the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) ) ) Element of bool [: the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
func InnerVertices G -> ( ( ) ( ) Subset of ) equals :: MSAFREE2:def 3
 rng the ResultSort of G : ( ( ) ( ) GrammarStr ) : ( ( Function-like V29( the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) -defined the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) -valued Function-like V29( the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) ) ) Element of bool [: the carrier' of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of G : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: MSAFREE2:1
for G being ( ( non empty void ) ( non empty void V55() trivial' ) ManySortedSign ) holds InputVertices G : ( ( non empty void ) ( non empty void V55() trivial' ) ManySortedSign ) : ( ( ) ( ) Subset of ) = the carrier of G : ( ( non empty void ) ( non empty void V55() trivial' ) ManySortedSign ) : ( ( ) ( non empty ) set ) ;

theorem :: MSAFREE2:2
for G being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for v being ( ( ) ( ) Vertex of G : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) st v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) in InputVertices G : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) holds
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) holds not the_result_sort_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;

theorem :: MSAFREE2:3
for G being ( ( non empty ) ( non empty V55() ) ManySortedSign ) holds SortsWithConstants G : ( ( non empty ) ( non empty V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) c= InnerVertices G : ( ( non empty ) ( non empty V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) ;

theorem :: MSAFREE2:4
for G being ( ( non empty ) ( non empty V55() ) ManySortedSign ) holds InputVertices G : ( ( non empty ) ( non empty V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) misses SortsWithConstants G : ( ( non empty ) ( non empty V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) ;

definition
let IT be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
attr IT is with_input_V means :: MSAFREE2:def 4
 InputVertices IT : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) ;
end;

registration
cluster non empty non void V55() with_input_V for ( ( ) ( ) ManySortedSign ) ;
end;

registration
let G be ( ( non empty with_input_V ) ( non empty V55() with_input_V ) ManySortedSign ) ;
cluster InputVertices G : ( ( non empty with_input_V ) ( non empty V55() with_input_V ) ManySortedSign ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

registration
let G be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
cluster InnerVertices G : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

definition
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
let MSA be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) ;
mode InputValues of MSA -> ( ( Relation-like InputVertices S : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ) -defined Function-like total ) ( Relation-like InputVertices S : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ) -defined Function-like total ) ManySortedSet of InputVertices S : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ) ) means :: MSAFREE2:def 5
 for v being ( ( ) ( ) Vertex of S : ( ( ) ( ) set ) ) st v : ( ( ) ( ) Vertex of S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) in InputVertices S : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ) holds
it : ( ( ) ( Relation-like S : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( ) ( ) set ) )) -valued ) Element of bool [:S : ( ( ) ( ) set ) ,(S : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) . v : ( ( ) ( ) Vertex of S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) : ( ( ) ( ) set ) in the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Vertex of S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) : ( ( ) ( ) set ) ;
end;

definition
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
attr S is Circuit-like means :: MSAFREE2:def 6
 for S9 being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) st S9 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) = S : ( ( ) ( ) set ) holds
for o1, o2 being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) st the_result_sort_of o1 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) = the_result_sort_of o2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) holds
o1 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) = o2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster non empty void -> non empty Circuit-like for ( ( ) ( ) ManySortedSign ) ;
end;

registration
cluster non empty non void V55() strict Circuit-like for ( ( ) ( ) ManySortedSign ) ;
end;

definition
let IIG be ( ( non empty non void Circuit-like ) ( non empty non void V55() Circuit-like ) ManySortedSign ) ;
let v be ( ( ) ( ) Vertex of IIG : ( ( non empty non void Circuit-like ) ( non empty non void V55() Circuit-like ) ManySortedSign ) ) ;
assume v : ( ( ) ( ) Vertex of IIG : ( ( non empty non void Circuit-like ) ( non empty non void V55() Circuit-like ) ManySortedSign ) ) in InnerVertices IIG : ( ( non empty non void Circuit-like ) ( non empty non void V55() Circuit-like ) ManySortedSign ) : ( ( ) ( non empty ) Subset of ) ;
func action_at v -> ( ( ) ( ) OperSymbol of ( ( ) ( ) set ) ) means :: MSAFREE2:def 7
 the_result_sort_of it : ( ( ) ( Relation-like IIG : ( ( ) ( ) set ) -defined IIG : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8(IIG : ( ( ) ( ) set ) )) -valued ) Element of bool [:IIG : ( ( ) ( ) set ) ,(IIG : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M8(IIG : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of IIG : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = v : ( ( ) ( ) set ) ;
end;

begin

theorem :: MSAFREE2:5
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for A being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for p being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence) st len p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = len (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & ( for k being ( ( V13() ) ( V7() V8() V9() V13() ) Nat) st k : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) in dom p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence) : ( ( ) ( finite countable ) Element of bool K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence) . k : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) : ( ( ) ( ) set ) in the Sorts of A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . ((the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) /. k : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence) in Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let S be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let MSA be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;
func FreeEnv MSA -> ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over S : ( ( ) ( ) set ) ) equals :: MSAFREE2:def 8
 FreeMSA the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( ) MSAlgebra over S : ( ( ) ( ) set ) ) ;
end;

definition
let S be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let MSA be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;
func Eval MSA -> ( ( ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V41() ) ManySortedFunction of S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) means :: MSAFREE2:def 9
( it : ( ( ) ( Relation-like S : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( ) ( ) set ) )) -valued ) Element of bool [:S : ( ( ) ( ) set ) ,(S : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is_homomorphism FreeEnv MSA : ( ( ) ( ) set ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over S : ( ( ) ( ) set ) ) ,MSA : ( ( ) ( ) set ) & ( for s being ( ( ) ( ) SortSymbol of ( ( ) ( ) set ) )
for x, y being ( ( ) ( ) set ) st y : ( ( ) ( ) set ) in FreeSort ( the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional constituted-DTrees ) Element of bool (TS (DTConMSA the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( ) DTConstrStr ) ) : ( ( ) ( functional constituted-DTrees ) Element of bool (FinTrees the carrier of (DTConMSA the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( ) DTConstrStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional constituted-DTrees ) DTree-set of the carrier of (DTConMSA the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( ) DTConstrStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & y : ( ( ) ( ) set ) = root-tree [x : ( ( ) ( ) set ) ,s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like finite countable DecoratedTree-like ) set ) & x : ( ( ) ( ) set ) in the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
(it : ( ( ) ( Relation-like S : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( ) ( ) set ) )) -valued ) Element of bool [:S : ( ( ) ( ) set ) ,(S : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V29( the Sorts of (FreeEnv MSA : ( ( ) ( ) set ) ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over S : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the Sorts of (FreeEnv MSA : ( ( ) ( ) set ) ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over S : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V29( the Sorts of (FreeEnv MSA : ( ( ) ( ) set ) ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over S : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Element of bool [:( the Sorts of (FreeEnv MSA : ( ( ) ( ) set ) ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over S : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,( the Sorts of MSA : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ) );
end;

theorem :: MSAFREE2:6
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) holds the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) is ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) GeneratorSet of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) ;

definition
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
let IT be ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) ;
attr IT is finitely-generated means :: MSAFREE2:def 10
 for S9 being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) st S9 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) = S : ( ( ) ( ) set ) holds
for A being ( ( ) ( ) MSAlgebra over S9 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) st A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) = IT : ( ( ) ( ) set ) holds
ex G being ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) GeneratorSet of A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) st G : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) GeneratorSet of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) is V33() if not S : ( ( ) ( ) set ) is void
otherwise the Sorts of IT : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) is V33();
end;

definition
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
let IT be ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) ;
attr IT is finite-yielding means :: MSAFREE2:def 11
 the Sorts of IT : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) is V33();
end;

registration
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
cluster non-empty finite-yielding -> non-empty finitely-generated for ( ( ) ( ) MSAlgebra over S : ( ( ) ( ) set ) ) ;
end;

definition
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
func Trivial_Algebra S -> ( ( strict ) ( strict ) MSAlgebra over S : ( ( ) ( ) set ) ) means :: MSAFREE2:def 12
 the Sorts of it : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) = the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) --> {0 : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) } : ( ( ) ( non empty functional finite V36() with_common_domain countable Tree-like ) set ) : ( ( Function-like V29( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,{{0 : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) } : ( ( ) ( non empty functional finite V36() with_common_domain countable Tree-like ) set ) } : ( ( ) ( non empty finite V36() countable ) set ) ) ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined {{0 : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) } : ( ( ) ( non empty functional finite V36() with_common_domain countable Tree-like ) set ) } : ( ( ) ( non empty finite V36() countable ) set ) -valued Function-like constant total V29( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,{{0 : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) } : ( ( ) ( non empty functional finite V36() with_common_domain countable Tree-like ) set ) } : ( ( ) ( non empty finite V36() countable ) set ) ) ) Element of bool [: the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,{{0 : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) } : ( ( ) ( non empty functional finite V36() with_common_domain countable Tree-like ) set ) } : ( ( ) ( non empty finite V36() countable ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let S be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
cluster strict non-empty finite-yielding for ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) ;
end;

definition
let IT be ( ( non empty ) ( non empty V55() ) ManySortedSign ) ;
attr IT is monotonic means :: MSAFREE2:def 13
 for A being ( ( non-empty finitely-generated ) ( non-empty finitely-generated ) MSAlgebra over IT : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) holds A : ( ( non-empty finitely-generated ) ( non-empty finitely-generated ) MSAlgebra over IT : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) is finite-yielding ;
end;

registration
cluster non empty finite non void V55() Circuit-like monotonic for ( ( ) ( ) ManySortedSign ) ;
end;

theorem :: MSAFREE2:7
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for X being ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )
for v being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds e : ( ( ) ( ) Element of the Sorts of (FreeMSA b2 : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( Relation-like Function-like finite DecoratedTree-like ) ( Relation-like Function-like finite countable DecoratedTree-like ) DecoratedTree) ;

theorem :: MSAFREE2:8
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for X being ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total V33() ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total V33() ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) holds FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total V33() ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total V33() ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) is finitely-generated ;

theorem :: MSAFREE2:9
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) )
for v being ( ( ) ( ) Vertex of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) )
for e being ( ( ) ( ) Element of the Sorts of (FreeEnv A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) in InputVertices S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( ) Subset of ) holds
ex x being ( ( ) ( ) Element of the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) st e : ( ( ) ( ) Element of the Sorts of (FreeEnv b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) : ( ( strict non-empty free ) ( strict non-empty free ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . b3 : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = root-tree [x : ( ( ) ( ) Element of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . b3 : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ] : ( ( ) ( ) set ) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like finite countable DecoratedTree-like ) set ) ;

theorem :: MSAFREE2:10
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for X being ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for p being ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) st [o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) , the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ] : ( ( ) ( ) set ) -tree p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) in the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . (the_result_sort_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) holds
len p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = len (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: MSAFREE2:11
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for X being ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for p being ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) st [o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) , the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ] : ( ( ) ( ) set ) -tree p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) in the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . (the_result_sort_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) holds
for i being ( ( V13() ) ( V7() V8() V9() V13() ) Nat) st i : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) in dom (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( finite countable ) Element of bool K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) . i : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) : ( ( ) ( ) set ) in the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . ((the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) . i : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

registration
let S be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let X be ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) Vertex of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;
cluster -> non empty Relation-like Function-like finite for ( ( ) ( ) Element of the Sorts of (FreeMSA X : ( ( ) ( ) set ) ) : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like the carrier of S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( Relation-like S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) -defined S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) * : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) )) -valued ) Element of bool [:S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) ,(S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) *) : ( ( ) ( non empty functional FinSequence-membered ) M8(S : ( ( non empty ) ( non empty V55() ) ManySortedSign ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let X be ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) Vertex of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;
cluster non empty Relation-like Function-like finite countable for ( ( ) ( ) Element of the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let X be ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) Vertex of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;
cluster Relation-like Function-like -> Relation-like Function-like DecoratedTree-like for ( ( ) ( ) Element of the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let IIG be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let X be ( ( Relation-like V16() the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) Vertex of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ;
cluster non empty Relation-like Function-like finite countable DecoratedTree-like for ( ( ) ( ) Element of the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Element of the carrier of IIG : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: MSAFREE2:12
for S being ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign )
for X being ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )
for v being ( ( ) ( ) Vertex of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( non empty Relation-like Function-like finite countable DecoratedTree-like ) Element of the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) st e : ( ( ) ( non empty Relation-like Function-like finite countable DecoratedTree-like ) Element of the Sorts of (FreeMSA b2 : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . b3 : ( ( ) ( ) Vertex of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) . {} : ( ( ) ( empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ) set ) : ( ( ) ( ) set ) = [o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) , the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ] : ( ( ) ( ) set ) holds
ex p being ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) st
( len p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = len (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & ( for i being ( ( V13() ) ( V7() V8() V9() V13() ) Nat) st i : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) in dom p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) : ( ( ) ( finite countable ) Element of bool K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( Relation-like Function-like FinSequence-like DTree-yielding ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding ) FinSequence) . i : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) : ( ( ) ( ) set ) in the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . ((the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) . i : ( ( V13() ) ( V7() V8() V9() V13() ) Nat) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

definition
let S be ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ;
let X be ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ;
let e be ( ( ) ( non empty Relation-like Function-like finite countable DecoratedTree-like ) Element of the Sorts of (FreeMSA X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . v : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
func depth e -> ( ( V13() ) ( V7() V8() V9() V13() ) Nat) means :: MSAFREE2:def 14
 ex dt being ( ( Relation-like Function-like finite DecoratedTree-like ) ( Relation-like Function-like finite countable DecoratedTree-like ) DecoratedTree) ex t being ( ( non empty finite Tree-like ) ( non empty finite countable Tree-like ) Tree) st
( dt : ( ( Relation-like Function-like finite DecoratedTree-like ) ( Relation-like Function-like finite countable DecoratedTree-like ) DecoratedTree) = e : ( ( Function-like V29(X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ,S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) ( Relation-like X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) -defined S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) -valued Function-like V29(X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ,S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) ) ) Element of bool [:X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ,S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & t : ( ( non empty finite Tree-like ) ( non empty finite countable Tree-like ) Tree) = dom dt : ( ( Relation-like Function-like finite DecoratedTree-like ) ( Relation-like Function-like finite countable DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty finite countable Tree-like ) set ) & it : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total Function-yielding V41() ) ManySortedFunction of the Sorts of X : ( ( Relation-like V16() the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like V16() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) , the Sorts of v : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V55() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) = height t : ( ( non empty finite Tree-like ) ( non empty finite countable Tree-like ) Tree) : ( ( ) ( V7() V8() V9() V13() ) Element of K37() : ( ( ) ( non empty non trivial V7() V8() V9() non finite countable denumerable ) Element of bool K33() : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) );
end;