:: Free Term Algebras
:: by Grzegorz Bancerek
::
:: Received May 15, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


theorem Th1: :: MSAFREE4:1
for I being set
for f1, f2 being ManySortedSet of I st f1 c= f2 holds
Union f1 c= Union f2
proof end;

deffunc H1( Function, set ) -> set = $1 . $2;

definition
let I be set ;
let X be V5() ManySortedSet of I;
let A be Component of X;
:: original: Element
redefine mode Element of A -> Element of Union X;
coherence
for b1 being Element of A holds b1 is Element of Union X
proof end;
end;

definition
let I be set ;
let X be ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func X . i -> Component of X;
coherence
X . i is Component of X
proof end;
end;

Lm1: now :: thesis: for I being set
for X, Y being ManySortedSet of I
for f being ManySortedFunction of X,Y
for x being object holds f . x is Function of (X . x),(Y . x)
let I be set ; :: thesis: for X, Y being ManySortedSet of I
for f being ManySortedFunction of X,Y
for x being object holds b8 . b9 is Function of (b6 . b9),(b7 . b9)
let X, Y be ManySortedSet of I; :: thesis: for f being ManySortedFunction of X,Y
for x being object holds b6 . b7 is Function of (b4 . b7),(b5 . b7)
let f be ManySortedFunction of X,Y; :: thesis: for x being object holds b5 . b6 is Function of (b3 . b6),(b4 . b6)
let x be object ; :: thesis: b4 . b5 is Function of (b2 . b5),(b3 . b5)
per cases ( x in I or x nin I ) ;
suppose x in I ; :: thesis: b4 . b5 is Function of (b2 . b5),(b3 . b5)
hence f . x is Function of (X . x),(Y . x) by PBOOLE:def 15; :: thesis: verum
end;
suppose A1: x nin I ; :: thesis: b4 . b5 is Function of (b2 . b5),(b3 . b5)
( dom f = I & dom X = I & dom Y = I ) by PARTFUN1:def 2;
then ( f . x = {} & X . x = {} & Y . x = {} & dom {} = {} & rng {} = {} ) by A1, FUNCT_1:def 2;
hence f . x is Function of (X . x),(Y . x) by FUNCT_2:2; :: thesis: verum
end;
end;
end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
let f be ManySortedFunction of X,Y;
let x be object ;
:: original: .
redefine func f . x -> Function of (X . x),(Y . x);
coherence
f . x is Function of (X . x),(Y . x) by Lm1;
end;

scheme :: MSAFREE4:sch 1
Sch1{ F1() -> set , F2() -> V5() ManySortedSet of F1(), F3( object , object ) -> set } :
ex f being ManySortedFunction of F1() st
for x being set st x in F1() holds
( dom (f . x) = F2() . x & ( for y being Element of F2() . x holds (f . x) . y = F3(x,y) ) )
proof end;

scheme :: MSAFREE4:sch 2
Sch2{ F1() -> non empty set , F2() -> V5() ManySortedSet of F1(), F3() -> V5() ManySortedSet of F1(), F4( object , object ) -> set } :
ex f being ManySortedFunction of F2(),F3() st
for i being Element of F1()
for a being Element of F2() . i holds (f . i) . a = F4(i,a)
provided
A1: for i being Element of F1()
for a being Element of F2() . i holds F4(i,a) in F3() . i
proof end;

definition
let X be non empty set ;
let O be set ;
let f be Function of O,X;
let g be ManySortedSet of X;
:: original: *
redefine func g * f -> ManySortedSet of O;
coherence
f * g is ManySortedSet of O ;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let F be ManySortedSet of S -Terms X;
let o be OperSymbol of S;
let p be ArgumentSeq of Sym (o,X);
cluster p * F -> FinSequence-like ;
coherence
F * p is FinSequence-like
proof end;
end;

theorem Th2: :: MSAFREE4:2
for x being set holds Subtrees (root-tree x) = {(root-tree x)}
proof end;

registration
let f be DTree-yielding Function;
cluster proj2 f -> constituted-DTrees ;
coherence
rng f is constituted-DTrees by TREES_3:def 11;
end;

theorem Th3: :: MSAFREE4:3
for x being set
for p being non empty DTree-yielding FinSequence holds Subtrees (x -tree p) = {(x -tree p)} \/ (Subtrees (rng p))
proof end;

theorem Th4: :: MSAFREE4:4
for x being set holds Subtrees (x -tree {}) = {(x -tree {})}
proof end;

theorem :: MSAFREE4:5
for x being set holds x -tree {} = root-tree x
proof end;

registration
cluster non empty Relation-like NAT -defined Function-like finite V32() FinSequence-like FinSubsequence-like DTree-yielding countable for set ;
existence
ex b1 being FinSequence st
( b1 is V32() & b1 is DTree-yielding & not b1 is empty )
proof end;
cluster non empty Relation-like NAT -defined Function-like finite V32() FinSequence-like FinSubsequence-like Tree-yielding countable for set ;
existence
ex b1 being FinSequence st
( b1 is V32() & b1 is Tree-yielding & not b1 is empty )
proof end;
end;

registration
let f be finite-yielding Function-yielding Function;
cluster doms f -> finite-yielding ;
coherence
doms f is finite-yielding
proof end;
end;

registration
let p be V32() Tree-yielding FinSequence;
cluster tree p -> finite ;
coherence
tree p is finite
proof end;
end;

registration
let t be finite DecoratedTree;
cluster Subtrees t -> finite-membered ;
coherence
Subtrees t is finite-membered ;
end;

registration
let p be V32() DTree-yielding FinSequence;
let x be set ;
cluster x -tree p -> finite ;
coherence
x -tree p is finite
proof end;
end;

theorem Th6: :: MSAFREE4:6
for t1, t2 being finite DecoratedTree st t1 in Subtrees t2 holds
height (dom t1) <= height (dom t2)
proof end;

theorem Th7: :: MSAFREE4:7
for x, y being set
for p being DTree-yielding FinSequence st p is V32() holds
for t being DecoratedTree st x in Subtrees t & t in rng p holds
x <> y -tree p
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of S;
cluster Relation-like S -Terms X -valued Function-like -> S -Terms X -valued finite-yielding for set ;
coherence
for b1 being S -Terms X -valued Function holds b1 is finite-yielding
proof end;
end;

theorem Th8: :: MSAFREE4:8
for X being non empty constituted-DTrees set
for t being DecoratedTree st t in X holds
Subtrees t c= Subtrees X
proof end;

theorem Th9: :: MSAFREE4:9
for X being non empty constituted-DTrees set holds X c= Subtrees X
proof end;

theorem Th10: :: MSAFREE4:10
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for t being Term of S,X
for x being set st x in Subtrees t holds
x is Term of S,X
proof end;

theorem Th11: :: MSAFREE4:11
for x being set
for p being DTree-yielding FinSequence holds rng p c= Subtrees (x -tree p)
proof end;

theorem Th12: :: MSAFREE4:12
for t1, t2 being DecoratedTree st t1 in Subtrees t2 holds
Subtrees t1 c= Subtrees t2
proof end;

theorem Th13: :: MSAFREE4:13
for S being non empty non void ManySortedSign
for X being ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) holds
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p
proof end;

registration
let I be set ;
let A, B be V5() ManySortedSet of I;
let f be ManySortedFunction of A,B;
cluster rngs f -> V5() ;
coherence
rngs f is non-empty
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
cluster -> Relation-like Function-like for Element of Union the Sorts of (TermAlg S);
coherence
for b1 being Element of (TermAlg S) holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

registration
let I be set ;
let A be ManySortedSet of I;
let f be FinSequence of I;
cluster f * A -> dom f -defined ;
coherence
A * f is dom f -defined
proof end;
end;

registration
let I be set ;
let A be ManySortedSet of I;
let f be FinSequence of I;
cluster f * A -> dom f -defined total for dom f -defined Relation;
coherence
for b1 being dom f -defined Relation st b1 = A * f holds
b1 is total
proof end;
end;

theorem :: MSAFREE4:14
for I being non empty set
for J being set
for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f
proof end;

theorem Th15: :: MSAFREE4:15
for I being set
for A, B being ManySortedSet of I st A c= B holds
for f being FinSequence of I holds A * f c= B * f
proof end;

theorem Th16: :: MSAFREE4:16
for I being set
for A, B being ManySortedSet of I st A c= B holds
product A c= product B
proof end;

theorem Th17: :: MSAFREE4:17
for x being set
for R being weakly-normalizing with_UN_property Relation st x is_a_normal_form_wrt R holds
nf (x,R) = x
proof end;

theorem Th18: :: MSAFREE4:18
for x being set
for R being weakly-normalizing with_UN_property Relation holds nf ((nf (x,R)),R) = nf (x,R)
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A be MSSubset of (FreeMSA X);
let x be object ;
cluster -> Relation-like Function-like for Element of A . x;
coherence
for b1 being Element of A . x holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

definition
let I be set ;
let A be ManySortedSet of I;
attr A is countable means :Def1: :: MSAFREE4:def 1
 for x being set st x in I holds
A . x is countable ;
end;

:: deftheorem Def1 defines countable MSAFREE4:def 1 :
for I being set
for A being ManySortedSet of I holds
( A is countable iff for x being set st x in I holds
A . x is countable );

registration
let I be set ;
let X be countable set ;
cluster I --> X -> countable for ManySortedSet of I;
coherence
for b1 being ManySortedSet of I st b1 = I --> X holds
b1 is countable by FUNCOP_1:7;
end;

registration
let I be set ;
cluster Relation-like V5() I -defined Function-like total countable for set ;
existence
ex b1 being ManySortedSet of I st
( b1 is V5() & b1 is countable )
proof end;
end;

registration
let I be set ;
let X be countable ManySortedSet of I;
let x be object ;
cluster X . x -> countable ;
coherence
X . x is countable
proof end;
end;

registration
let A be countable set ;
cluster Relation-like A -defined NAT -valued Function-like one-to-one V18(A, NAT ) for Element of bool [:A,NAT:];
existence
ex b1 being Function of A,NAT st b1 is one-to-one
proof end;
end;

registration
let I be set ;
let X0 be countable ManySortedSet of I;
cluster Relation-like I -defined Function-like total Function-yielding Relation-yielding "1-1" for ManySortedFunction of X0,I --> NAT;
existence
ex b1 being ManySortedFunction of X0,I --> NAT st b1 is "1-1"
proof end;
end;

theorem Th19: :: MSAFREE4:19
for S being set
for X being ManySortedSet of S
for Y being V5() ManySortedSet of S
for w being ManySortedFunction of X,Y holds rngs w is ManySortedSubset of Y
proof end;

theorem :: MSAFREE4:20
for S being set
for X being countable ManySortedSet of S ex Y being ManySortedSubset of S --> NAT ex w being ManySortedFunction of X,S --> NAT st
( w is "1-1" & Y = rngs w & ( for x being set st x in S holds
( w . x is Enumeration of (X . x) & Y . x = card (X . x) ) ) )
proof end;

theorem Th21: :: MSAFREE4:21
for I being set
for A being ManySortedSet of I
for B being V5() ManySortedSet of I holds A is_transformable_to B
proof end;

theorem Th22: :: MSAFREE4:22
for I being set
for A, B, C being V5() ManySortedSet of I
for f being ManySortedFunction of A,B st B is ManySortedSubset of C holds
f is ManySortedFunction of A,C
proof end;

theorem Th23: :: MSAFREE4:23
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of A,B st f is "onto" holds
ex g being ManySortedFunction of B,A st f ** g = id B
proof end;

Lm2: now :: thesis: for p being FinSequence
for i being Nat st i < len p holds
i + 1 in dom p
let p be FinSequence; :: thesis: for i being Nat st i < len p holds
i + 1 in dom p
let i be Nat; :: thesis: ( i < len p implies i + 1 in dom p )
assume i < len p ; :: thesis: i + 1 in dom p
then ( i + 1 <= len p & 1 <= i + 1 ) by NAT_1:13, NAT_1:11;
hence i + 1 in dom p by FINSEQ_3:25; :: thesis: verum
end;

theorem Th24: :: MSAFREE4:24
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 holds
for o being OperSymbol of S st B1 is_closed_on o holds
B2 is_closed_on o ;

theorem Th25: :: MSAFREE4:25
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 holds
for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. B1
proof end;

theorem Th26: :: MSAFREE4:26
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
Opers (A2,B2) = Opers (A1,B1)
proof end;

theorem Th27: :: MSAFREE4:27
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
B2 is opers_closed by Th24;

theorem :: MSAFREE4:28
for S being non empty non void ManySortedSign
for A1, A2, B being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubAlgebra of A1 st MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) holds
B is MSSubAlgebra of A2
proof end;

theorem :: MSAFREE4:29
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st A2 is empty holds
for h being ManySortedFunction of A1,A2 holds h is_homomorphism A1,A2
proof end;

theorem Th30: :: MSAFREE4:30
for S being non empty non void ManySortedSign
for A1, A2, B1 being MSAlgebra over S
for B2 being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2
proof end;

definition
let I be set ;
let X be ManySortedSet of I;
:: original: trivial-yielding
redefine attr X is trivial-yielding means :Def2: :: MSAFREE4:def 2
 for x being set st x in I holds
X . x is trivial ;
compatibility
( X is trivial-yielding iff for x being set st x in I holds
X . x is trivial )
proof end;
end;

:: deftheorem Def2 defines trivial-yielding MSAFREE4:def 2 :
for I being set
for X being ManySortedSet of I holds
( X is trivial-yielding iff for x being set st x in I holds
X . x is trivial );

registration
let I be set ;
cluster Relation-like V5() I -defined Function-like total V276() for set ;
existence
ex b1 being ManySortedSet of I st
( b1 is V5() & b1 is V276() )
proof end;
end;

registration
let I be set ;
let S be V276() ManySortedSet of I;
let x be object ;
cluster S . x -> trivial ;
coherence
S . x is trivial
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
attr A is trivial means :Def3: :: MSAFREE4:def 3
 the Sorts of A is V276();
end;

:: deftheorem Def3 defines trivial MSAFREE4:def 3 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds
( A is trivial iff the Sorts of A is V276() );

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

registration
let S be non empty non void ManySortedSign ;
let A be trivial MSAlgebra over S;
cluster the Sorts of A -> V276() ;
coherence
the Sorts of A is trivial-yielding by Def3;
end;

theorem Th31: :: MSAFREE4:31
for S being non empty non void ManySortedSign
for A being non-empty trivial MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds A |= e
proof end;

theorem Th32: :: MSAFREE4:32
for S being non empty non void ManySortedSign
for A being non-empty trivial MSAlgebra over S
for T being EqualSet of S holds A |= T by Th31;

theorem Th33: :: MSAFREE4:33
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for T being non-empty trivial MSAlgebra over S
for f being ManySortedFunction of A,T holds f is_homomorphism A,T
proof end;

theorem Th34: :: MSAFREE4:34
for S being non empty non void ManySortedSign
for T being non-empty trivial MSAlgebra over S
for A being non-empty MSSubAlgebra of T holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of T, the Charact of T #)
proof end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let C be MSAlgebra over S;
attr C is A -Image means :: MSAFREE4:def 4
 ex B being non-empty MSAlgebra over S ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h );
end;

:: deftheorem defines -Image MSAFREE4:def 4 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSAlgebra over S holds
( C is A -Image iff ex B being non-empty MSAlgebra over S ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h ) );

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster A -Image -> non-empty for MSAlgebra over S;
coherence
for b1 being MSAlgebra over S st b1 is A -Image holds
b1 is non-empty
proof end;
cluster strict non-empty feasible non empty A -Image for MSAlgebra over S;
existence
ex b1 being strict non-empty MSAlgebra over S st b1 is A -Image
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let A, C be non-empty MSAlgebra over S;
redefine attr C is A -Image means :Def5: :: MSAFREE4:def 5
 ex h being ManySortedFunction of A,C st h is_epimorphism A,C;
compatibility
( C is A -Image iff ex h being ManySortedFunction of A,C st h is_epimorphism A,C )
proof end;
end;

:: deftheorem Def5 defines -Image MSAFREE4:def 5 :
for S being non empty non void ManySortedSign
for A, C being non-empty MSAlgebra over S holds
( C is A -Image iff ex h being ManySortedFunction of A,C st h is_epimorphism A,C );

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
mode image of A is non-empty A -Image MSAlgebra over S;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster non-empty disjoint_valued feasible non empty trivial A -Image for MSAlgebra over S;
existence
ex b1 being image of A st
( b1 is disjoint_valued & b1 is trivial )
proof end;
end;

theorem Th35: :: MSAFREE4:35
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for B being b2 -Image MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st A |= e holds
B |= e
proof end;

theorem Th36: :: MSAFREE4:36
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for B being b2 -Image MSAlgebra over S
for T being EqualSet of S st A |= T holds
B |= T by Th35;

definition
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A be MSAlgebra over S;
attr A is X,S -terms means :Def6: :: MSAFREE4:def 6
 the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X));
end;

:: deftheorem Def6 defines -terms MSAFREE4:def 6 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being MSAlgebra over S holds
( A is X,S -terms iff the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) );

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster Free (S,X) -> X,S -terms ;
coherence
Free (S,X) is X,S -terms
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster Free (S,X) -> non-empty disjoint_valued ;
coherence
( Free (S,X) is non-empty & Free (S,X) is disjoint_valued )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster strict non-empty X,S -terms for MSAlgebra over S;
existence
ex b1 being strict MSAlgebra over S st
( b1 is X,S -terms & b1 is non-empty )
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A be X,S -terms MSAlgebra over S;
attr A is all_vars_including means :Def7: :: MSAFREE4:def 7
 FreeGen X is ManySortedSubset of the Sorts of A;
attr A is inheriting_operations means :Def8: :: MSAFREE4:def 8
 for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p );
attr A is free_in_itself means :Def9: :: MSAFREE4:def 9
 for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G );
end;

:: deftheorem Def7 defines all_vars_including MSAFREE4:def 7 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms MSAlgebra over S holds
( A is all_vars_including iff FreeGen X is ManySortedSubset of the Sorts of A );

:: deftheorem Def8 defines inheriting_operations MSAFREE4:def 8 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms MSAlgebra over S holds
( A is inheriting_operations iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) );

:: deftheorem Def9 defines free_in_itself MSAFREE4:def 9 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms MSAlgebra over S holds
( A is free_in_itself iff for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G ) );

theorem :: MSAFREE4:37
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) & A is X,S -terms holds
B is X,S -terms ;

theorem :: MSAFREE4:38
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A, B being non-empty b2,b1 -terms MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )
proof end;

registration
let J be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over J;
cluster non empty Relation-like V5() the carrier of J -defined Function-like total for GeneratorSet of T;
existence
not for b1 being GeneratorSet of T holds b1 is V5()
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster Free (S,X) -> all_vars_including inheriting_operations free_in_itself ;
coherence
( Free (S,X) is all_vars_including & Free (S,X) is inheriting_operations & Free (S,X) is free_in_itself )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster X,S -terms all_vars_including -> non-empty X,S -terms for MSAlgebra over S;
coherence
for b1 being X,S -terms MSAlgebra over S st b1 is all_vars_including holds
b1 is non-empty
proof end;
cluster strict X,S -terms all_vars_including inheriting_operations free_in_itself for MSAlgebra over S;
existence
ex b1 being strict X,S -terms MSAlgebra over S st
( b1 is all_vars_including & b1 is inheriting_operations & b1 is free_in_itself )
proof end;
end;

theorem Th39: :: MSAFREE4:39
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b2,b1 -terms MSAlgebra over S holds
( ( for t being Element of A0 holds t is Element of (Free (S,X)) ) & ( for s being SortSymbol of S
for t being Element of A0,s holds t is Element of (Free (S,X)),s ) )
proof end;

theorem Th40: :: MSAFREE4:40
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b2,b1 -terms all_vars_including MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A1,s
proof end;

theorem Th41: :: MSAFREE4:41
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b2,b1 -terms all_vars_including MSAlgebra over S
for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))
proof end;

registration
let S be set ;
cluster Relation-like V5() S -defined Function-like total disjoint_valued for set ;
existence
ex b1 being ManySortedSet of S st
( b1 is disjoint_valued & b1 is V5() )
proof end;
end;

registration
let S be set ;
let T be V5() disjoint_valued ManySortedSet of S;
cluster -> disjoint_valued for ManySortedSubset of T;
coherence
for b1 being ManySortedSubset of T holds b1 is disjoint_valued
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster strict X,S -terms for MSAlgebra over S;
existence
ex b1 being MSAlgebra over S st
( b1 is X,S -terms & b1 is strict )
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A1 be X,S -terms all_vars_including MSAlgebra over S;
func canonical_homomorphism A1 -> ManySortedFunction of (Free (S,X)),A1 means :Def10: :: MSAFREE4:def 10
( it is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = it || G ) );
existence
ex b1 being ManySortedFunction of (Free (S,X)),A1 st
( b1 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b1 || G ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (Free (S,X)),A1 st b1 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b1 || G ) & b2 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b2 || G ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines canonical_homomorphism MSAFREE4:def 10 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b2,b1 -terms all_vars_including MSAlgebra over S
for b4 being ManySortedFunction of (Free (S,X)),A1 holds
( b4 = canonical_homomorphism A1 iff ( b4 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b4 || G ) ) );

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A0 be non-empty X,S -terms MSAlgebra over S;
cluster -> Relation-like Function-like for Element of Union the Sorts of A0;
coherence
for b1 being Element of A0 holds
( b1 is Function-like & b1 is Relation-like )
proof end;
let s be SortSymbol of S;
cluster -> Relation-like Function-like for Element of the Sorts of A0 . s;
coherence
for b1 being Element of A0,s holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A0 be non-empty X,S -terms MSAlgebra over S;
cluster -> DecoratedTree-like for Element of Union the Sorts of A0;
coherence
for b1 being Element of A0 holds b1 is DecoratedTree-like
proof end;
let s be SortSymbol of S;
cluster -> DecoratedTree-like for Element of the Sorts of A0 . s;
coherence
for b1 being Element of A0,s holds b1 is DecoratedTree-like
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster X,S -terms -> disjoint_valued for MSAlgebra over S;
coherence
for b1 being MSAlgebra over S st b1 is X,S -terms holds
b1 is disjoint_valued
proof end;
end;

theorem Th42: :: MSAFREE4:42
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b2,b1 -terms MSAlgebra over S
for t being Element of A0 holds t is Term of S,X
proof end;

theorem Th43: :: MSAFREE4:43
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b2,b1 -terms MSAlgebra over S
for t being Element of A0
for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A0 . s
proof end;

theorem :: MSAFREE4:44
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S
for t being Element of A2
for p being Element of dom t holds t | p is Element of A2
proof end;

theorem Th45: :: MSAFREE4:45
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen X is GeneratorSet of A2
proof end;

theorem :: MSAFREE4:46
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for T being non-empty b2,b1 -terms free_in_itself MSAlgebra over S
for A being image of T
for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
proof end;

theorem Th47: :: MSAFREE4:47
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S holds
( canonical_homomorphism A2 is_epimorphism Free (S,X),A2 & ( for s being SortSymbol of S
for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t ) )
proof end;

theorem Th48: :: MSAFREE4:48
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S holds (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2
proof end;

theorem :: MSAFREE4:49
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A is Free (S,X) -Image
proof end;

theorem :: MSAFREE4:50
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t being Element of (TermAlg S),s holds A |= t '=' t ;

theorem :: MSAFREE4:51
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1, t2 being Element of (TermAlg S),s st A |= t1 '=' t2 holds
A |= t2 '=' t1 ;

theorem :: MSAFREE4:52
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1, t2, t3 being Element of (TermAlg S),s st A |= t1 '=' t2 & A |= t2 '=' t3 holds
A |= t1 '=' t3
proof end;

theorem :: MSAFREE4:53
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a1, a2 being FinSequence st a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) holds
for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2
proof end;

definition
let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
let A be MSAlgebra over S;
attr A is T -satisfying means :Def11: :: MSAFREE4:def 11
A |= T;
end;

:: deftheorem Def11 defines -satisfying MSAFREE4:def 11 :
for S being non empty non void ManySortedSign
for T being EqualSet of S
for A being MSAlgebra over S holds
( A is T -satisfying iff A |= T );

registration
let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
cluster non-empty trivial T -satisfying for MSAlgebra over S;
existence
ex b1 being MSAlgebra over S st
( b1 is T -satisfying & b1 is non-empty & b1 is trivial )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
let A be non-empty T -satisfying MSAlgebra over S;
cluster non-empty A -Image -> non-empty T -satisfying for MSAlgebra over S;
coherence
for b1 being non-empty MSAlgebra over S st b1 is A -Image holds
b1 is T -satisfying by Def11, Th36;
end;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let T be EqualSet of S;
let G be GeneratorSet of A;
attr G is T -free means :: MSAFREE4:def 12
 for B being non-empty T -satisfying MSAlgebra over S
for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & h || G = f );
end;

:: deftheorem defines -free MSAFREE4:def 12 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for T being EqualSet of S
for G being GeneratorSet of A holds
( G is T -free iff for B being non-empty b3 -satisfying MSAlgebra over S
for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & h || G = f ) );

definition
let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
let A be MSAlgebra over S;
attr A is T -free means :: MSAFREE4:def 13
 ex G being GeneratorSet of A st G is T -free ;
end;

:: deftheorem defines -free MSAFREE4:def 13 :
for S being non empty non void ManySortedSign
for T being EqualSet of S
for A being MSAlgebra over S holds
( A is T -free iff ex G being GeneratorSet of A st G is T -free );

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
func Equations (S,A) -> EqualSet of S means :Def14: :: MSAFREE4:def 14
 for s being SortSymbol of S holds it . s = { e where e is Element of (Equations S) . s : A |= e } ;
existence
ex b1 being EqualSet of S st
for s being SortSymbol of S holds b1 . s = { e where e is Element of (Equations S) . s : A |= e }
proof end;
uniqueness
for b1, b2 being EqualSet of S st ( for s being SortSymbol of S holds b1 . s = { e where e is Element of (Equations S) . s : A |= e } ) & ( for s being SortSymbol of S holds b2 . s = { e where e is Element of (Equations S) . s : A |= e } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines Equations MSAFREE4:def 14 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for b3 being EqualSet of S holds
( b3 = Equations (S,A) iff for s being SortSymbol of S holds b3 . s = { e where e is Element of (Equations S) . s : A |= e } );

theorem Th54: :: MSAFREE4:54
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds A |= Equations (S,A)
proof end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster A -Image -> A -Image Equations (S,A) -satisfying for MSAlgebra over S;
coherence
for b1 being A -Image MSAlgebra over S holds b1 is Equations (S,A) -satisfying
proof end;
end;

scheme :: MSAFREE4:sch 3
TermDefEx{ F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of F1(), F3( set , set ) -> set , F4( set , set ) -> set } :
ex F being ManySortedSet of F1() -Terms F2() st
( ( for s being SortSymbol of F1()
for x being Element of F2() . s holds F . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) holds F . ((Sym (o,F2())) -tree p) = F4(o,(F * p)) ) )
proof end;

scheme :: MSAFREE4:sch 4
TermDefUniq{ F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of F1(), F3( set , set ) -> set , F4( set , FinSequence) -> set , F5() -> ManySortedSet of F1() -Terms F2(), F6() -> ManySortedSet of F1() -Terms F2() } :
F5() = F6()
provided
A1: for s being SortSymbol of F1()
for x being Element of F2() . s holds F5() . (root-tree [x,s]) = F3(x,s) and
A2: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) holds F5() . ((Sym (o,F2())) -tree p) = F4(o,(F5() * p)) and
A3: for s being SortSymbol of F1()
for x being Element of F2() . s holds F6() . (root-tree [x,s]) = F3(x,s) and
A4: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) holds F6() . ((Sym (o,F2())) -tree p) = F4(o,(F6() * p))
proof end;

definition
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let w be ManySortedFunction of X, the carrier of S --> NAT;
let t be Function;
assume A1: t is Element of (Free (S,X)) ;
deffunc H2( set , set ) -> set = root-tree [((w . $2) . $1),$2];
deffunc H3( OperSymbol of S, FinSequence) -> set = (Sym ($1,( the carrier of S --> NAT))) -tree $2;
func # (t,w) -> Element of (TermAlg S) means :Def15: :: MSAFREE4:def 15
 ex F being ManySortedSet of S -Terms X st
( it = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) );
existence
ex b1 being Element of (TermAlg S) ex F being ManySortedSet of S -Terms X st
( b1 = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) )
proof end;
uniqueness
for b1, b2 being Element of (TermAlg S) st ex F being ManySortedSet of S -Terms X st
( b1 = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) & ex F being ManySortedSet of S -Terms X st
( b2 = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines # MSAFREE4:def 15 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Function st t is Element of (Free (S,X)) holds
for b5 being Element of (TermAlg S) holds
( b5 = # (t,w) iff ex F being ManySortedSet of S -Terms X st
( b5 = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) );

theorem Th55: :: MSAFREE4:55
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for F being ManySortedSet of S -Terms X st ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) holds
for t being Element of (Free (S,X)) holds F . t = # (t,w)
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let G be V5() MSSubset of (Free (S,X));
let s be SortSymbol of S;
cluster -> Relation-like Function-like for Element of G . s;
coherence
for b1 being Element of G . s holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

theorem Th56: :: MSAFREE4:56
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
proof end;

theorem Th57: :: MSAFREE4:57
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for s being SortSymbol of S
for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]
proof end;

theorem Th58: :: MSAFREE4:58
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
proof end;

theorem Th59: :: MSAFREE4:59
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for Y being ManySortedSubset of X holds Free (S,Y) is MSSubAlgebra of Free (S,X)
proof end;

theorem Th60: :: MSAFREE4:60
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Term of S,X holds
( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )
proof end;

theorem :: MSAFREE4:61
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for F being ManySortedSet of S -Terms X st ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) holds
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds
( F * p in Args (o,(Free (S,(rngs w)))) & F * p in Args (o,(Free (S,( the carrier of S --> NAT)))) )
proof end;

theorem Th62: :: MSAFREE4:62
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of the carrier of S --> NAT,X ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )
proof end;

theorem Th63: :: MSAFREE4:63
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
proof end;

theorem :: MSAFREE4:64
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (TermAlg S),A0 st h is_homomorphism TermAlg S,A0 holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex Y being V5() ManySortedSubset of the carrier of S --> NAT ex B being MSSubset of (TermAlg S) ex ww being ManySortedFunction of (Free (S,Y)),A0 ex g being ManySortedFunction of A0,A0 st
( Y = rngs w & B = the Sorts of (Free (S,Y)) & FreeGen (rngs w) c= B & ww is_homomorphism Free (S,Y),A0 & g is_homomorphism A0,A0 & h || B = g ** ww & ( for s being SortSymbol of S
for i being Nat st i in Y . s holds
ex x being Element of X0 . s st
( (w . s) . x = i & (ww . s) . (root-tree [i,s]) = root-tree [x,s] ) ) )
proof end;

theorem Th65: :: MSAFREE4:65
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
proof end;

theorem Th66: :: MSAFREE4:66
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A)
for x0 being Element of Args (o,(Free (S,X))) st x0 = x holds
(canonical_homomorphism A) # x0 = x
proof end;

theorem Th67: :: MSAFREE4:67
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
proof end;

theorem Th68: :: MSAFREE4:68
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
proof end;

theorem Th69: :: MSAFREE4:69
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))
proof end;

theorem :: MSAFREE4:70
for S being non empty non void ManySortedSign
for X0, Y0 being V5() countable ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S
for h being ManySortedFunction of (Free (S,Y0)),A st h is_homomorphism Free (S,Y0),A holds
ex g being ManySortedFunction of (Free (S,Y0)),(Free (S,X0)) st
( g is_homomorphism Free (S,Y0), Free (S,X0) & h = (canonical_homomorphism A) ** g & ( for G being GeneratorSet of Free (S,Y0) st G = FreeGen Y0 holds
g || G = h || G ) )
proof end;

theorem Th71: :: MSAFREE4:71
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
proof end;

theorem :: MSAFREE4:72
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
proof end;

theorem Th73: :: MSAFREE4:73
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )
proof end;

theorem Th74: :: MSAFREE4:74
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for B being non-empty MSAlgebra over S
for h being ManySortedFunction of (Free (S,X0)),B st h is_homomorphism Free (S,X0),B holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & B |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
proof end;

theorem Th75: :: MSAFREE4:75
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
proof end;

theorem :: MSAFREE4:76
for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A0 is Equations (S,A0) -free
proof end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
let R be ManySortedRelation of X,Y;
let x be object ;
:: original: .
redefine func R . x -> Relation of (X . x),(Y . x);
coherence
R . x is Relation of (X . x),(Y . x)
proof end;
end;

definition
let I be set ;
let X be ManySortedSet of I;
let R be ManySortedRelation of X;
attr R is terminating means :Def16: :: MSAFREE4:def 16
 for x being set st x in I holds
R . x is strongly-normalizing ;
attr R is with_UN_property means :Def17: :: MSAFREE4:def 17
 for x being set st x in I holds
R . x is with_UN_property ;
end;

:: deftheorem Def16 defines terminating MSAFREE4:def 16 :
for I being set
for X being ManySortedSet of I
for R being ManySortedRelation of X holds
( R is terminating iff for x being set st x in I holds
R . x is strongly-normalizing );

:: deftheorem Def17 defines with_UN_property MSAFREE4:def 17 :
for I being set
for X being ManySortedSet of I
for R being ManySortedRelation of X holds
( R is with_UN_property iff for x being set st x in I holds
R . x is with_UN_property );

registration
cluster empty -> empty strongly-normalizing with_UN_property for set ;
coherence
for b1 being empty set holds
( b1 is strongly-normalizing & b1 is with_UN_property ) ;
end;

theorem Th77: :: MSAFREE4:77
for I being set
for A being ManySortedSet of I ex R being ManySortedRelation of A st
( R = I --> {} & R is terminating )
proof end;

registration
let I be set ;
let X be ManySortedSet of I;
cluster V6() -> terminating with_UN_property for ManySortedRelation of X,X;
coherence
for b1 being ManySortedRelation of X st b1 is V6() holds
( b1 is with_UN_property & b1 is terminating ) ;
cluster Relation-like V6() I -defined Function-like total Relation-yielding for ManySortedRelation of X,X;
existence
not for b1 being ManySortedRelation of X holds b1 is V6()
proof end;
end;

registration
let I be set ;
let X be ManySortedSet of I;
let R be terminating ManySortedRelation of X;
let i be object ;
cluster R . i -> strongly-normalizing for Relation;
coherence
for b1 being Relation st b1 = R . i holds
b1 is strongly-normalizing
proof end;
end;

registration
let I be set ;
let X be ManySortedSet of I;
let R be with_UN_property ManySortedRelation of X;
let i be object ;
cluster R . i -> with_UN_property for Relation;
coherence
for b1 being Relation st b1 = R . i holds
b1 is with_UN_property
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be ManySortedRelation of (Free (S,X));
attr R is NF-var means :Def18: :: MSAFREE4:def 18
 for s being SortSymbol of S
for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s;
end;

:: deftheorem Def18 defines NF-var MSAFREE4:def 18 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being ManySortedRelation of (Free (S,X)) holds
( R is NF-var iff for s being SortSymbol of S
for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s );

theorem :: MSAFREE4:78
for x being set holds x is_a_normal_form_wrt {} ;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster V6() -> invariant stable NF-var for ManySortedRelation of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));
coherence
for b1 being ManySortedRelation of (Free (S,X)) st b1 is V6() holds
( b1 is NF-var & b1 is invariant & b1 is stable )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding invariant stable terminating with_UN_property NF-var for ManySortedRelation of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));
existence
ex b1 being invariant stable ManySortedRelation of (Free (S,X)) st
( b1 is NF-var & b1 is terminating & b1 is with_UN_property )
proof end;
end;

scheme :: MSAFREE4:sch 5
A{ F1() -> set , F2() -> set , F3() -> Relation, P1[ set ] } :
P1[F2()]
provided
A1: P1[F1()] and
A2: F3() reduces F1(),F2() and
A3: for y, z being set st F3() reduces F1(),y & [y,z] in F3() & P1[y] holds
P1[z]
proof end;

scheme :: MSAFREE4:sch 6
B{ F1() -> set , F2() -> set , F3() -> Relation, P1[ set ] } :
P1[F1()]
provided
A1: P1[F2()] and
A2: F3() reduces F1(),F2() and
A3: for y, z being set st [y,z] in F3() & P1[z] holds
P1[y]
proof end;

definition
let X be non empty set ;
let R be strongly-normalizing with_UN_property Relation of X;
let x be Element of X;
:: original: nf
redefine func nf (x,R) -> Element of X;
coherence
nf (x,R) is Element of X
proof end;
end;

definition
let I be non empty set ;
let X be V5() ManySortedSet of I;
let R be terminating with_UN_property ManySortedRelation of X;
func NForms R -> V5() ManySortedSubset of X means :Def19: :: MSAFREE4:def 19
 for i being Element of I holds it . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ;
existence
ex b1 being V5() ManySortedSubset of X st
for i being Element of I holds b1 . i = { (nf (x,(R . i))) where x is Element of X . i : verum }
proof end;
uniqueness
for b1, b2 being V5() ManySortedSubset of X st ( for i being Element of I holds b1 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) & ( for i being Element of I holds b2 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines NForms MSAFREE4:def 19 :
for I being non empty set
for X being V5() ManySortedSet of I
for R being terminating with_UN_property ManySortedRelation of X
for b4 being V5() ManySortedSubset of X holds
( b4 = NForms R iff for i being Element of I holds b4 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } );

scheme :: MSAFREE4:sch 7
MSFLambda{ F1() -> non empty set , F2( object ) -> non empty set , F3( object , object ) -> set } :
ex f being ManySortedFunction of F1() st
for o being Element of F1() holds
( dom (f . o) = F2(o) & ( for x being Element of F2(o) holds (f . o) . x = F3(o,x) ) )
proof end;

definition
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X));
func NFAlgebra R -> strict non-empty MSAlgebra over S means :Def20: :: MSAFREE4:def 20
( the Sorts of it = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,it) holds (Den (o,it)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) );
existence
ex b1 being strict non-empty MSAlgebra over S st
( the Sorts of b1 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b1) holds (Den (o,b1)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) )
proof end;
uniqueness
for b1, b2 being strict non-empty MSAlgebra over S st the Sorts of b1 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b1) holds (Den (o,b1)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) & the Sorts of b2 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b2) holds (Den (o,b2)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines NFAlgebra MSAFREE4:def 20 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for b4 being strict non-empty MSAlgebra over S holds
( b4 = NFAlgebra R iff ( the Sorts of b4 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b4) holds (Den (o,b4)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) ) );

theorem Th79: :: MSAFREE4:79
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for x being set
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x
proof end;

Lm3: now :: thesis: for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let X be V5() ManySortedSet of S; :: thesis: for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X)); :: thesis: for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let o be OperSymbol of S; :: thesis: Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
set A = NFAlgebra R;
A1: the Sorts of (NFAlgebra R) = NForms R by Def20;
(NForms R) * (the_arity_of o) c= the Sorts of (Free (S,X)) * (the_arity_of o) by Th15, PBOOLE:def 18;
then product ((NForms R) * (the_arity_of o)) c= product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by Th16;
then product ((NForms R) * (the_arity_of o)) c= Args (o,(Free (S,X))) by PRALG_2:3;
hence Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) by A1, PRALG_2:3; :: thesis: verum
end;

theorem Th80: :: MSAFREE4:80
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
proof end;

theorem Th81: :: MSAFREE4:81
for p being FinSequence holds
( p /^ 0 = p & ( for i being Nat st i >= len p holds
p /^ i = {} ) )
proof end;

theorem Th82: :: MSAFREE4:82
for x, y being set
for p, q being FinSequence holds ((p ^ <*x*>) ^ q) +* (((len p) + 1),y) = (p ^ <*y*>) ^ q
proof end;

theorem Th83: :: MSAFREE4:83
for p being FinSequence
for i being Nat st i + 1 <= len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
proof end;

theorem Th84: :: MSAFREE4:84
for p being FinSequence
for i being Nat st i + 1 <= len p holds
p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1))
proof end;

theorem Th85: :: MSAFREE4:85
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X));
cluster NFAlgebra R -> strict non-empty X,S -terms ;
coherence
NFAlgebra R is X,S -terms
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X));
cluster NFAlgebra R -> strict non-empty all_vars_including inheriting_operations free_in_itself ;
coherence
( NFAlgebra R is all_vars_including & NFAlgebra R is inheriting_operations & NFAlgebra R is free_in_itself )
proof end;
end;