:: Free Many Sorted Universal Algebra
:: by Beata Perkowska
::
:: Received April 27, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

::
:: Preliminaries
::
theorem Th1: :: MSAFREE:1
for I being set
for J being non empty set
for f being Function of I,(J *)
for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
proofend;

definition
let I be set ;
let A, B be ManySortedSet of I;
let C be ManySortedSubset of A;
let F be ManySortedFunction of A,B;
funcF || C ->  ManySortedFunction of C,B means :Def1: :: MSAFREE:def 1
 for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
it . i = f | (C . i);
existence
 ex b1 being ManySortedFunction of C,B st
for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b1 . i = f | (C . i)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of C,B st ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b1 . i = f | (C . i) ) & ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b2 . i = f | (C . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines || MSAFREE:def_1_:_
 for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for b6 being ManySortedFunction of C,B holds
( b6 = F || C iff for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b6 . i = f | (C . i) );

definition
let I be set ;
let X be ManySortedSet of I;
let i be set ;
assume A1: i in I ;
func coprod (i,X) ->  set  means :Def2: :: MSAFREE:def 2
 for x being set holds
( x in it iff ex a being set st
( a in X . i & x = [a,i] ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex a being set st
( a in X . i & x = [a,i] ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . i & x = [a,i] ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . i & x = [a,i] ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines coprod MSAFREE:def_2_:_
 for I being set
for X being ManySortedSet of I
for i being set st i in I holds
for b4 being set holds
( b4 = coprod (i,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . i & x = [a,i] ) ) );

notation
let I be set ;
let X be ManySortedSet of I;
synonym  coprod X for  disjoin I;
end;

registration
let I be set ;
let X be ManySortedSet of I;
cluster coprod  -> I -defined ;
coherence
 coprod is I -defined
proofend;
end;

registration
let I be set ;
let X be ManySortedSet of I;
cluster coprod  ->  total ;
coherence
 coprod is total
proofend;
end;

definition
let I be set ;
let X be ManySortedSet of I;
:: original:coprod
redefine func coprod X ->  set  means :Def3: :: MSAFREE:def 3
( dom it = I & ( for i being set st i in I holds
it . i = coprod (i,X) ) );
compatibility
 for b1 being set holds
( b1 = coprod iff ( dom b1 = I & ( for i being set st i in I holds
b1 . i = coprod (i,X) ) ) )
proofend;
end;

:: deftheorem Def3 defines coprod MSAFREE:def_3_:_
 for I being set
for X being ManySortedSet of I
for b3 being set holds
( b3 = coprod X iff ( dom b3 = I & ( for i being set st i in I holds
b3 . i = coprod (i,X) ) ) );

registration
let I be non empty set ;
let X be V16() ManySortedSet of I;
cluster coprod  -> V16() ;
coherence
 coprod X is non-empty
proofend;
end;

registration
let I be non empty set ;
let X be V16() ManySortedSet of I;
cluster Union X ->  non empty ;
coherence
 not Union X is empty
proofend;
end;

theorem :: MSAFREE:2
for I being set
for X being ManySortedSet of I
for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )
proofend;

begin

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
mode GeneratorSet of U0 ->  MSSubset of U0 means :Def4: :: MSAFREE:def 4
 the Sorts of (GenMSAlg it) = the Sorts of U0;
existence
 ex b1 being MSSubset of U0 st the Sorts of (GenMSAlg b1) = the Sorts of U0
proofend;
end;

:: deftheorem Def4 defines GeneratorSet MSAFREE:def_4_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b3 being MSSubset of U0 holds
( b3 is GeneratorSet of U0 iff the Sorts of (GenMSAlg b3) = the Sorts of U0 );

theorem :: MSAFREE:3
for S being non empty non void ManySortedSign
for U0 being strict non-empty MSAlgebra over S
for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
proofend;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let IT be GeneratorSet of U0;
attrIT is free  means :Def5: :: MSAFREE:def 5
 for U1 being non-empty MSAlgebra over S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 &amp; h || IT = f );
end;

:: deftheorem Def5 defines free MSAFREE:def_5_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being non-empty MSAlgebra over S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 &amp; h || IT = f ) );

definition
let S be non empty non void ManySortedSign ;
let IT be MSAlgebra over S;
attrIT is free  means :Def6: :: MSAFREE:def 6
 ex G being GeneratorSet of IT st G is free ;
end;

:: deftheorem Def6 defines free MSAFREE:def_6_:_
 for S being non empty non void ManySortedSign
for IT being MSAlgebra over S holds
( IT is free iff ex G being GeneratorSet of IT st G is free );

theorem Th4: :: MSAFREE:4
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
proofend;

begin

::
:: Construction of Free Many Sorted Algebras for Given Signature
::
definition
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
func REL X ->  Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) means :Def7: :: MSAFREE:def 7
 for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) &amp; ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) );
existence
 ex b1 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st
for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) &amp; ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) &amp; ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) &amp; ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b2 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) &amp; ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines REL MSAFREE:def_7_:_
 for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for b3 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) holds
( b3 = REL X iff for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b3 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) &amp; ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) );

theorem Th5: :: MSAFREE:5
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) &amp; ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) &amp; ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
proofend;

definition
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
func DTConMSA X ->  DTConstrStr  equals :: MSAFREE:def 8
 DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);
correctness
coherence
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #) is DTConstrStr ;
;
end;

:: deftheorem  defines DTConMSA MSAFREE:def_8_:_
 for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

registration
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
cluster DTConMSA X ->  non empty strict ;
coherence
 ( DTConMSA X is strict &amp; not DTConMSA X is empty ) ;
end;

theorem Th6: :: MSAFREE:6
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds
( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] &amp; Union (coprod X) c= Terminals (DTConMSA X) &amp; ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] &amp; Terminals (DTConMSA X) = Union (coprod X) ) ) )
proofend;

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster DTConMSA X ->  with_terminals with_nonterminals with_useful_nonterminals ;
coherence
 ( DTConMSA X is with_terminals &amp; DTConMSA X is with_nonterminals &amp; DTConMSA X is with_useful_nonterminals )
proofend;
end;

theorem Th7: :: MSAFREE:7
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for t being set holds
( ( t in Terminals (DTConMSA X) &amp; X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s &amp; t = [x,s] ) ) &amp; ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
proofend;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
func Sym (o,X) ->  Symbol of (DTConMSA X) equals :: MSAFREE:def 9
[o, the carrier of S];
coherence
 [o, the carrier of S] is Symbol of (DTConMSA X)
proofend;
end;

:: deftheorem  defines Sym MSAFREE:def_9_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S holds Sym (o,X) = [o, the carrier of S];

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func FreeSort (X,s) ->  Subset of (TS (DTConMSA X)) equals :: MSAFREE:def 10
 {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s &amp; a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; the_result_sort_of o = s ) )  }  ;
coherence
  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s &amp; a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; the_result_sort_of o = s ) )  }  is Subset of (TS (DTConMSA X))
proofend;
end;

:: deftheorem  defines FreeSort MSAFREE:def_10_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (X,s) =  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s &amp; a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; the_result_sort_of o = s ) )  }  ;

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
cluster FreeSort (X,s) ->  non empty ;
coherence
 not FreeSort (X,s) is empty
proofend;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeSort X ->  ManySortedSet of the carrier of S means :Def11: :: MSAFREE:def 11
 for s being SortSymbol of S holds it . s = FreeSort (X,s);
existence
 ex b1 being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b1 . s = FreeSort (X,s)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = FreeSort (X,s) ) &amp; ( for s being SortSymbol of S holds b2 . s = FreeSort (X,s) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines FreeSort MSAFREE:def_11_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedSet of the carrier of S holds
( b3 = FreeSort X iff for s being SortSymbol of S holds b3 . s = FreeSort (X,s) );

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster FreeSort X -> V16() ;
coherence
 FreeSort X is non-empty
proofend;
end;

theorem Th8: :: MSAFREE:8
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
proofend;

theorem Th9: :: MSAFREE:9
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) &amp; ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
proofend;

theorem Th10: :: MSAFREE:10
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
proofend;

theorem Th11: :: MSAFREE:11
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)
proofend;

theorem Th12: :: MSAFREE:12
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
proofend;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
func DenOp (o,X) ->  Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) means :Def12: :: MSAFREE:def 12
 for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
it . p = (Sym (o,X)) -tree p;
existence
 ex b1 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st
for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b1 . p = (Sym (o,X)) -tree p
proofend;
uniqueness
 for b1, b2 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b1 . p = (Sym (o,X)) -tree p ) &amp; ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b2 . p = (Sym (o,X)) -tree p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines DenOp MSAFREE:def_12_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for b4 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) holds
( b4 = DenOp (o,X) iff for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b4 . p = (Sym (o,X)) -tree p );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeOper X ->  ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S means :Def13: :: MSAFREE:def 13
 for o being OperSymbol of S holds it . o = DenOp (o,X);
existence
 ex b1 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = DenOp (o,X)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = DenOp (o,X) ) &amp; ( for o being OperSymbol of S holds b2 . o = DenOp (o,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines FreeOper MSAFREE:def_13_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S holds
( b3 = FreeOper X iff for o being OperSymbol of S holds b3 . o = DenOp (o,X) );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeMSA X ->  MSAlgebra over S equals :: MSAFREE:def 14
 MSAlgebra(# (FreeSort X),(FreeOper X) #);
coherence
 MSAlgebra(# (FreeSort X),(FreeOper X) #) is MSAlgebra over S ;
end;

:: deftheorem  defines FreeMSA MSAFREE:def_14_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #);

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster FreeMSA X ->  strict non-empty ;
coherence
 ( FreeMSA X is strict &amp; FreeMSA X is non-empty ) by MSUALG_1:def_3;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func FreeGen (s,X) ->  Subset of ((FreeSort X) . s) means :Def15: :: MSAFREE:def 15
 for x being set holds
( x in it iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) );
existence
 ex b1 being Subset of ((FreeSort X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) )
proofend;
uniqueness
 for b1, b2 being Subset of ((FreeSort X) . s) st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines FreeGen MSAFREE:def_15_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Subset of ((FreeSort X) . s) holds
( b4 = FreeGen (s,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) ) );

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
cluster FreeGen (s,X) ->  non empty ;
coherence
 not FreeGen (s,X) is empty
proofend;
end;

theorem Th13: :: MSAFREE:13
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeGen (s,X) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) &amp; t `2 = s )  }
proofend;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeGen X ->  GeneratorSet of FreeMSA X means :Def16: :: MSAFREE:def 16
 for s being SortSymbol of S holds it . s = FreeGen (s,X);
existence
 ex b1 being GeneratorSet of FreeMSA X st
for s being SortSymbol of S holds b1 . s = FreeGen (s,X)
proofend;
uniqueness
 for b1, b2 being GeneratorSet of FreeMSA X st ( for s being SortSymbol of S holds b1 . s = FreeGen (s,X) ) &amp; ( for s being SortSymbol of S holds b2 . s = FreeGen (s,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines FreeGen MSAFREE:def_16_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being GeneratorSet of FreeMSA X holds
( b3 = FreeGen X iff for s being SortSymbol of S holds b3 . s = FreeGen (s,X) );

theorem :: MSAFREE:14
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeGen X is V16()
proofend;

theorem :: MSAFREE:15
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeGen X)) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }
proofend;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func Reverse (s,X) ->  Function of (FreeGen (s,X)),(X . s) means :Def17: :: MSAFREE:def 17
 for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
it . (root-tree t) = t `1 ;
existence
 ex b1 being Function of (FreeGen (s,X)),(X . s) st
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b1 . (root-tree t) = t `1
proofend;
uniqueness
 for b1, b2 being Function of (FreeGen (s,X)),(X . s) st ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b1 . (root-tree t) = t `1 ) &amp; ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b2 . (root-tree t) = t `1 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines Reverse MSAFREE:def_17_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Function of (FreeGen (s,X)),(X . s) holds
( b4 = Reverse (s,X) iff for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b4 . (root-tree t) = t `1 );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func Reverse X ->  ManySortedFunction of FreeGen X,X means :Def18: :: MSAFREE:def 18
 for s being SortSymbol of S holds it . s = Reverse (s,X);
existence
 ex b1 being ManySortedFunction of FreeGen X,X st
for s being SortSymbol of S holds b1 . s = Reverse (s,X)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of FreeGen X,X st ( for s being SortSymbol of S holds b1 . s = Reverse (s,X) ) &amp; ( for s being SortSymbol of S holds b2 . s = Reverse (s,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines Reverse MSAFREE:def_18_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedFunction of FreeGen X,X holds
( b3 = Reverse X iff for s being SortSymbol of S holds b3 . s = Reverse (s,X) );

definition
let S be non empty non void ManySortedSign ;
let X, A be V16() ManySortedSet of the carrier of S;
let F be ManySortedFunction of FreeGen X,A;
let t be Symbol of (DTConMSA X);
assume A1: t in Terminals (DTConMSA X) ;
func pi (F,A,t) ->  Element of Union A means :Def19: :: MSAFREE:def 19
 for f being Function st f = F . (t `2) holds
it = f . (root-tree t);
existence
 ex b1 being Element of Union A st
for f being Function st f = F . (t `2) holds
b1 = f . (root-tree t)
proofend;
uniqueness
 for b1, b2 being Element of Union A st ( for f being Function st f = F . (t `2) holds
b1 = f . (root-tree t) ) &amp; ( for f being Function st f = F . (t `2) holds
b2 = f . (root-tree t) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines pi MSAFREE:def_19_:_
 for S being non empty non void ManySortedSign
for X, A being V16() ManySortedSet of the carrier of S
for F being ManySortedFunction of FreeGen X,A
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
for b6 being Element of Union A holds
( b6 = pi (F,A,t) iff for f being Function st f = F . (t `2) holds
b6 = f . (root-tree t) );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let t be Symbol of (DTConMSA X);
assume A1: ex p being FinSequence st t ==> p ;
func @ (X,t) ->  OperSymbol of S means :Def20: :: MSAFREE:def 20
[it, the carrier of S] = t;
existence
 ex b1 being OperSymbol of S st [b1, the carrier of S] = t
proofend;
uniqueness
 for b1, b2 being OperSymbol of S st [b1, the carrier of S] = t &amp; [b2, the carrier of S] = t holds
b1 = b2 by XTUPLE_0:1;
end;

:: deftheorem Def20 defines @ MSAFREE:def_20_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for t being Symbol of (DTConMSA X) st ex p being FinSequence st t ==> p holds
for b4 being OperSymbol of S holds
( b4 = @ (X,t) iff [b4, the carrier of S] = t );

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let o be OperSymbol of S;
let p be FinSequence;
assume A1: p in Args (o,U0) ;
func pi (o,U0,p) ->  Element of Union the Sorts of U0 equals :Def21: :: MSAFREE:def 21
(Den (o,U0)) . p;
coherence
 (Den (o,U0)) . p is Element of Union the Sorts of U0
proofend;
end;

:: deftheorem Def21 defines pi MSAFREE:def_21_:_
 for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,U0) holds
pi (o,U0,p) = (Den (o,U0)) . p;

theorem Th16: :: MSAFREE:16
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free
proofend;

theorem Th17: :: MSAFREE:17
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free
proofend;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty free for MSAlgebra over S;
existence
 ex b1 being non-empty MSAlgebra over S st
( b1 is free &amp; b1 is strict )
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be free MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total free for GeneratorSet of U0;
existence
 ex b1 being GeneratorSet of U0 st b1 is free by Def6;
end;

theorem Th18: :: MSAFREE:18
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
proofend;

theorem :: MSAFREE:19
for S being non empty non void ManySortedSign
for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 &amp; Image F = U1 )
proofend;