:: Translations, Endomorphisms, and Stable Equational Theories
:: by Grzegorz Bancerek
::
:: Received February 9, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let S be non empty ManySortedSign ;
let A be MSAlgebra over S;
let s be SortSymbol of S;
mode Element of A,s is Element of the Sorts of A . s;
end;

definition
let I be set ;
let A be ManySortedSet of I;
let h1, h2 be ManySortedFunction of A,A;
:: original:**
redefine funch2 ** h1 ->  ManySortedFunction of A,A;
coherence
 h2 ** h1 is ManySortedFunction of A,A
proofend;
end;

theorem Th1: :: MSUALG_6:1
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for o being OperSymbol of S
for a being set st a in Args (o,A) holds
a is Function
proofend;

theorem Th2: :: MSUALG_6:2
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for o being OperSymbol of S
for a being Function st a in Args (o,A) holds
( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
a . i in the Sorts of A . ((the_arity_of o) /. i) ) )
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
attrA is feasible  means :Def1: :: MSUALG_6:def 1
 for o being OperSymbol of S st Args (o,A) <> {} holds
Result (o,A) <> {} ;
end;

:: deftheorem Def1 defines feasible MSUALG_6:def_1_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds
( A is feasible iff for o being OperSymbol of S st Args (o,A) <> {} holds
Result (o,A) <> {} );

theorem Th3: :: MSUALG_6:3
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds
( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} )
proofend;

registration
let S be non empty non void ManySortedSign ;
cluster non-empty  ->  feasible for MSAlgebra over S;
coherence
 for b1 being MSAlgebra over S st b1 is non-empty holds
b1 is feasible
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
cluster non-empty for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st b1 is non-empty
proofend;
end;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
mode Endomorphism of A ->  ManySortedFunction of A,A means :Def2: :: MSUALG_6:def 2
it is_homomorphism A,A;
existence
 ex b1 being ManySortedFunction of A,A st b1 is_homomorphism A,A
proofend;
end;

:: deftheorem Def2 defines Endomorphism MSUALG_6:def_2_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for b3 being ManySortedFunction of A,A holds
( b3 is Endomorphism of A iff b3 is_homomorphism A,A );

theorem Th4: :: MSUALG_6:4
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds id the Sorts of A is Endomorphism of A
proofend;

theorem Th5: :: MSUALG_6:5
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for h1, h2 being ManySortedFunction of A,A
for o being OperSymbol of S
for a being Element of Args (o,A) st a in Args (o,A) holds
h2 # (h1 # a) = (h2 ** h1) # a
proofend;

theorem Th6: :: MSUALG_6:6
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let h1, h2 be Endomorphism of A;
:: original:**
redefine funch2 ** h1 ->  Endomorphism of A;
coherence
 h2 ** h1 is Endomorphism of A by Th6;
end;

definition
let S be non empty non void ManySortedSign ;
func TranslationRel S ->  Relation of the carrier of S means :Def3: :: MSUALG_6:def 3
 for s1, s2 being SortSymbol of S holds
( [s1,s2] in it iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 ) ) );
existence
 ex b1 being Relation of the carrier of S st
for s1, s2 being SortSymbol of S holds
( [s1,s2] in b1 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 ) ) )
proofend;
correctness
uniqueness
for b1, b2 being Relation of the carrier of S st ( for s1, s2 being SortSymbol of S holds
( [s1,s2] in b1 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 ) ) ) ) &amp; ( for s1, s2 being SortSymbol of S holds
( [s1,s2] in b2 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 ) ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def3 defines TranslationRel MSUALG_6:def_3_:_
 for S being non empty non void ManySortedSign
for b2 being Relation of the carrier of S holds
( b2 = TranslationRel S iff for s1, s2 being SortSymbol of S holds
( [s1,s2] in b2 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 ) ) ) );

theorem Th7: :: MSUALG_6:7
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S
for a being Function st a in Args (o,A) holds
for i being Element of NAT
for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A)
proofend;

theorem Th8: :: MSUALG_6:8
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for o being OperSymbol of S st Args (o,A1) <> {} &amp; Args (o,A2) <> {} holds
for i being Element of NAT st i in dom (the_arity_of o) holds
for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)
proofend;

theorem Th9: :: MSUALG_6:9
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) &amp; h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a &amp; g1 = h # a &amp; g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x &amp; h # b = g1 +* (i,(g2 . i)) )
proofend;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let i be Element of NAT ;
let A be MSAlgebra over S;
let a be Function;
func transl (o,i,a,A) ->  Function means :Def4: :: MSUALG_6:def 4
( dom it = the Sorts of A . ((the_arity_of o) /. i) &amp; ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
it . x = (Den (o,A)) . (a +* (i,x)) ) );
existence
 ex b1 being Function st
( dom b1 = the Sorts of A . ((the_arity_of o) /. i) &amp; ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b1 . x = (Den (o,A)) . (a +* (i,x)) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = the Sorts of A . ((the_arity_of o) /. i) &amp; ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b1 . x = (Den (o,A)) . (a +* (i,x)) ) &amp; dom b2 = the Sorts of A . ((the_arity_of o) /. i) &amp; ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b2 . x = (Den (o,A)) . (a +* (i,x)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines transl MSUALG_6:def_4_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Element of NAT
for A being MSAlgebra over S
for a, b6 being Function holds
( b6 = transl (o,i,a,A) iff ( dom b6 = the Sorts of A . ((the_arity_of o) /. i) &amp; ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b6 . x = (Den (o,A)) . (a +* (i,x)) ) ) );

theorem Th10: :: MSUALG_6:10
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Element of NAT
for A being feasible MSAlgebra over S
for a being Function st a in Args (o,A) holds
transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o))
proofend;

definition
let S be non empty non void ManySortedSign ;
let s1, s2 be SortSymbol of S;
let A be MSAlgebra over S;
let f be Function;
predf is_e.translation_of A,s1,s2 means :Def5: :: MSUALG_6:def 5
 ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 &amp; ex a being Function st
( a in Args (o,A) &amp; f = transl (o,i,a,A) ) ) );
end;

:: deftheorem Def5 defines is_e.translation_of MSUALG_6:def_5_:_
 for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being MSAlgebra over S
for f being Function holds
( f is_e.translation_of A,s1,s2 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 &amp; ex i being Element of NAT st
( i in dom (the_arity_of o) &amp; (the_arity_of o) /. i = s1 &amp; ex a being Function st
( a in Args (o,A) &amp; f = transl (o,i,a,A) ) ) ) );

theorem Th11: :: MSUALG_6:11
for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being feasible MSAlgebra over S
for f being Function st f is_e.translation_of A,s1,s2 holds
( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) &amp; the Sorts of A . s1 <> {} &amp; the Sorts of A . s2 <> {} )
proofend;

theorem Th12: :: MSUALG_6:12
for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being MSAlgebra over S
for f being Function st f is_e.translation_of A,s1,s2 holds
[s1,s2] in TranslationRel S
proofend;

theorem :: MSUALG_6:13
for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds
ex f being Function st f is_e.translation_of A,s1,s2
proofend;

theorem Th14: :: MSUALG_6:14
for S being non empty non void ManySortedSign
for A being feasible MSAlgebra over S
for s1, s2 being SortSymbol of S
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 &amp; s1 = q . 1 &amp; s2 = q . (len q) &amp; ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p &amp; f = p . i &amp; s1 = q . i &amp; s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) &amp; ( p <> {} implies ( the Sorts of A . s1 <> {} &amp; the Sorts of A . s2 <> {} ) ) )
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let s1, s2 be SortSymbol of S;
assume B1: TranslationRel S reduces s1,s2 ;
mode Translation of A,s1,s2 ->  Function of ( the Sorts of A . s1),( the Sorts of A . s2) means :Def6: :: MSUALG_6:def 6
 ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( it = compose (p,( the Sorts of A . s1)) &amp; len q = (len p) + 1 &amp; s1 = q . 1 &amp; s2 = q . (len q) &amp; ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p &amp; f = p . i &amp; s1 = q . i &amp; s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) );
existence
 ex b1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( b1 = compose (p,( the Sorts of A . s1)) &amp; len q = (len p) + 1 &amp; s1 = q . 1 &amp; s2 = q . (len q) &amp; ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p &amp; f = p . i &amp; s1 = q . i &amp; s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) )
proofend;
end;

:: deftheorem Def6 defines Translation MSUALG_6:def_6_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for b5 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) holds
( b5 is Translation of A,s1,s2 iff ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( b5 = compose (p,( the Sorts of A . s1)) &amp; len q = (len p) + 1 &amp; s1 = q . 1 &amp; s2 = q . (len q) &amp; ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p &amp; f = p . i &amp; s1 = q . i &amp; s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) ) );

theorem :: MSUALG_6:15
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 &amp; s1 = q . 1 &amp; s2 = q . (len q) &amp; ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p &amp; f = p . i &amp; s1 = q . i &amp; s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2
proofend;

theorem Th16: :: MSUALG_6:16
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S holds id ( the Sorts of A . s) is Translation of A,s,s
proofend;

theorem Th17: :: MSUALG_6:17
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S
for f being Function st f is_e.translation_of A,s1,s2 holds
( TranslationRel S reduces s1,s2 &amp; f is Translation of A,s1,s2 )
proofend;

theorem Th18: :: MSUALG_6:18
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 &amp; TranslationRel S reduces s2,s3 holds
for t1 being Translation of A,s1,s2
for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3
proofend;

theorem Th19: :: MSUALG_6:19
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2
for f being Function st f is_e.translation_of A,s2,s3 holds
f * t is Translation of A,s1,s3
proofend;

theorem :: MSUALG_6:20
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s2,s3 holds
for f being Function st f is_e.translation_of A,s1,s2 holds
for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3
proofend;

scheme :: MSUALG_6:sch 1
TranslationInd{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), P1[ set , set , set ] } :
 for s1, s2 being SortSymbol of F1() st TranslationRel F1() reduces s1,s2 holds
for t being Translation of F2(),s1,s2 holds P1[t,s1,s2]
provided
A1: for s being SortSymbol of F1() holds P1[ id ( the Sorts of F2() . s),s,s] and
A2: for s1, s2, s3 being SortSymbol of F1() st TranslationRel F1() reduces s1,s2 holds
for t being Translation of F2(),s1,s2 st P1[t,s1,s2] holds
for f being Function st f is_e.translation_of F2(),s2,s3 holds
P1[f * t,s1,s3]
proofend;

theorem Th21: :: MSUALG_6:21
for S being non empty non void ManySortedSign
for A1, A2 being non-empty MSAlgebra over S
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i))
proofend;

theorem :: MSUALG_6:22
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for h being Endomorphism of A
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args (o,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i))
proofend;

theorem Th23: :: MSUALG_6:23
for S being non empty non void ManySortedSign
for A1, A2 being non-empty MSAlgebra over S
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A1,s1,s2 holds
ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st
( T is_e.translation_of A2,s1,s2 &amp; T * (h . s1) = (h . s2) * t )
proofend;

theorem :: MSUALG_6:24
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for h being Endomorphism of A
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st
( T is_e.translation_of A,s1,s2 &amp; T * (h . s1) = (h . s2) * t )
proofend;

theorem Th25: :: MSUALG_6:25
for S being non empty non void ManySortedSign
for A1, A2 being non-empty MSAlgebra over S
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t
proofend;

theorem Th26: :: MSUALG_6:26
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for h being Endomorphism of A
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t
proofend;

begin

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let R be ManySortedRelation of A;
attrR is compatible  means :Def7: :: MSUALG_6:def 7
 for o being OperSymbol of S
for a, b being Function st a in Args (o,A) &amp; b in Args (o,A) &amp; ( for n being Element of NAT st n in dom (the_arity_of o) holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o);
attrR is invariant  means :Def8: :: MSUALG_6:def 8
 for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2;
attrR is stable  means :Def9: :: MSUALG_6:def 9
 for h being Endomorphism of A
for s being SortSymbol of S
for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s;
end;

:: deftheorem Def7 defines compatible MSUALG_6:def_7_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for R being ManySortedRelation of A holds
( R is compatible iff for o being OperSymbol of S
for a, b being Function st a in Args (o,A) &amp; b in Args (o,A) &amp; ( for n being Element of NAT st n in dom (the_arity_of o) holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) );

:: deftheorem Def8 defines invariant MSUALG_6:def_8_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 );

:: deftheorem Def9 defines stable MSUALG_6:def_9_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for R being ManySortedRelation of A holds
( R is stable iff for h being Endomorphism of A
for s being SortSymbol of S
for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s );

theorem :: MSUALG_6:27
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of A holds
( R is compatible iff R is MSCongruence of A )
proofend;

theorem Th28: :: MSUALG_6:28
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
proofend;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster MSEquivalence-like invariant  ->  MSEquivalence-like compatible for ManySortedRelation of the Sorts of A, the Sorts of A;
coherence
 for b1 being MSEquivalence-like ManySortedRelation of A st b1 is invariant holds
b1 is compatible
proofend;
cluster MSEquivalence-like compatible  ->  MSEquivalence-like invariant for ManySortedRelation of the Sorts of A, the Sorts of A;
coherence
 for b1 being MSEquivalence-like ManySortedRelation of A st b1 is compatible holds
b1 is invariant
proofend;
end;

registration
let X be non empty set ;
cluster id X ->  non empty ;
coherence
 not id X is empty ;
end;

scheme :: MSUALG_6:sch 2
MSRExistence{ F1() ->  non empty set , F2() ->  V16() ManySortedSet of F1(), P1[ set , set , set ] } :
 ex R being ManySortedRelation of F2() st
for i being Element of F1()
for a, b being Element of F2() . i holds
( [a,b] in R . i iff P1[i,a,b] )
proofend;

scheme :: MSUALG_6:sch 3
MSRLambdaU{ F1() ->  set , F2() ->  ManySortedSet of F1(), F3( set ) ->  set } :
 ( ex R being ManySortedRelation of F2() st
for i being set st i in F1() holds
R . i = F3(i) &amp; ( for R1, R2 being ManySortedRelation of F2() st ( for i being set st i in F1() holds
R1 . i = F3(i) ) &amp; ( for i being set st i in F1() holds
R2 . i = F3(i) ) holds
R1 = R2 ) )
provided
A1: for i being set st i in F1() holds
F3(i) is Relation of (F2() . i),(F2() . i)
proofend;

definition
let I be set ;
let A be ManySortedSet of I;
func id (I,A) ->  ManySortedRelation of A means :Def10: :: MSUALG_6:def 10
 for i being set st i in I holds
it . i = id (A . i);
correctness
existence
ex b1 being ManySortedRelation of A st
for i being set st i in I holds
b1 . i = id (A . i);
uniqueness
for b1, b2 being ManySortedRelation of A st ( for i being set st i in I holds
b1 . i = id (A . i) ) &amp; ( for i being set st i in I holds
b2 . i = id (A . i) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def10 defines id MSUALG_6:def_10_:_
 for I being set
for A being ManySortedSet of I
for b3 being ManySortedRelation of A holds
( b3 = id (I,A) iff for i being set st i in I holds
b3 . i = id (A . i) );

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster MSEquivalence-like  -> V16() for ManySortedRelation of the Sorts of A, the Sorts of A;
coherence
 for b1 being ManySortedRelation of A st b1 is MSEquivalence-like holds
b1 is V16()
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like invariant stable for ManySortedRelation of the Sorts of A, the Sorts of A;
existence
 ex b1 being ManySortedRelation of A st
( b1 is invariant &amp; b1 is stable &amp; b1 is MSEquivalence-like )
proofend;
end;

begin

scheme :: MSUALG_6:sch 4
MSRelCl{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), P1[ set , set , set ], P2[ set ], F3() ->  ManySortedRelation of F2(), F4() ->  ManySortedRelation of F2() } :
 ( P2[F4()] &amp; F3() c= F4() &amp; ( for P being ManySortedRelation of F2() st P2[P] &amp; F3() c= P holds
F4() c= P ) )
provided
A1: for R being ManySortedRelation of F2() holds
( P2[R] iff for s1, s2 being SortSymbol of F1()
for f being Function of ( the Sorts of F2() . s1),( the Sorts of F2() . s2) st P1[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) and
A2: for s1, s2, s3 being SortSymbol of F1()
for f1 being Function of ( the Sorts of F2() . s1),( the Sorts of F2() . s2)
for f2 being Function of ( the Sorts of F2() . s2),( the Sorts of F2() . s3) st P1[f1,s1,s2] &amp; P1[f2,s2,s3] holds
P1[f2 * f1,s1,s3] and
A3: for s being SortSymbol of F1() holds P1[ id ( the Sorts of F2() . s),s,s] and
A4: for s being SortSymbol of F1()
for a, b being Element of F2(),s holds
( [a,b] in F4() . s iff ex s9 being SortSymbol of F1() ex f being Function of ( the Sorts of F2() . s9),( the Sorts of F2() . s) ex x, y being Element of F2(),s9 st
( P1[f,s9,s] &amp; [x,y] in F3() . s9 &amp; a = f . x &amp; b = f . y ) )
proofend;

Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_A_being_non-empty_MSAlgebra_over_S
for_R,_Q_being_ManySortedRelation_of_A_st_(_for_s_being_SortSymbol_of_S
for_a,_b_being_Element_of_A,s_holds_
(_[a,b]_in_Q_._s_iff_ex_s9_being_SortSymbol_of_S_ex_f_being_Function_of_(_the_Sorts_of_A_._s9),(_the_Sorts_of_A_._s)_ex_x,_y_being_Element_of_A,s9_st_
(_S2[f,s9,s]_&amp;_[x,y]_in_R_._s9_&amp;_a_=_f_._x_&amp;_b_=_f_._y_)_)_)_holds_
(_S1[Q]_&amp;_R_c=_Q_&amp;_(_for_P_being_ManySortedRelation_of_A_st_S1[P]_&amp;_R_c=_P_holds_
Q_c=_P_)_)
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ) holds
( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) )
let A be non-empty MSAlgebra over S; ::_thesis: for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ) holds
( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) )
let R, Q be ManySortedRelation of A; ::_thesis: ( ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ) implies ( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) ) )
defpred S1[ ManySortedRelation of A] means $1 is invariant ;
defpred S2[ Function, SortSymbol of S, SortSymbol of S] means ( TranslationRel S reduces $2,$3 &amp; $1 is Translation of A,$2,$3 );
assume A1: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ; ::_thesis: ( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) )
A2: for s being SortSymbol of S holds S2[ id ( the Sorts of A . s),s,s] by Th16, REWRITE1:12;
A3: now__::_thesis:_for_R_being_ManySortedRelation_of_A_holds_
(_(_S1[R]_implies_for_s1,_s2_being_SortSymbol_of_S
for_f_being_Function_of_(_the_Sorts_of_A_._s1),(_the_Sorts_of_A_._s2)_st_S2[f,s1,s2]_holds_
for_a,_b_being_set_st_[a,b]_in_R_._s1_holds_
[(f_._a),(f_._b)]_in_R_._s2_)_&amp;_(_(_for_s1,_s2_being_SortSymbol_of_S
for_f_being_Function_of_(_the_Sorts_of_A_._s1),(_the_Sorts_of_A_._s2)_st_S2[f,s1,s2]_holds_
for_a,_b_being_set_st_[a,b]_in_R_._s1_holds_
[(f_._a),(f_._b)]_in_R_._s2_)_implies_S1[R]_)_)
let R be ManySortedRelation of A; ::_thesis: ( ( S1[R] implies for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) &amp; ( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] ) )
thus  ( S1[R] implies for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) by Th28; ::_thesis: ( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] )
assume  for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ; ::_thesis: S1[R]
then  for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ;
hence  S1[R] by Th28; ::_thesis: verum
end;
A4: for s1, s2, s3 being SortSymbol of S
for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2)
for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] &amp; S2[f2,s2,s3] holds
S2[f2 * f1,s1,s3] by Th18, REWRITE1:16;
thus  ( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) ) from MSUALG_6:sch_4(A3, A4, A2, A1); ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be ManySortedRelation of the Sorts of A;
func InvCl R ->  invariant ManySortedRelation of A means :Def11: :: MSUALG_6:def 11
( R c= it &amp; ( for Q being invariant ManySortedRelation of A st R c= Q holds
it c= Q ) );
uniqueness
 for b1, b2 being invariant ManySortedRelation of A st R c= b1 &amp; ( for Q being invariant ManySortedRelation of A st R c= Q holds
b1 c= Q ) &amp; R c= b2 &amp; ( for Q being invariant ManySortedRelation of A st R c= Q holds
b2 c= Q ) holds
b1 = b2
proofend;
existence
 ex b1 being invariant ManySortedRelation of A st
( R c= b1 &amp; ( for Q being invariant ManySortedRelation of A st R c= Q holds
b1 c= Q ) )
proofend;
end;

:: deftheorem Def11 defines InvCl MSUALG_6:def_11_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for b4 being invariant ManySortedRelation of A holds
( b4 = InvCl R iff ( R c= b4 &amp; ( for Q being invariant ManySortedRelation of A st R c= Q holds
b4 c= Q ) ) );

theorem Th29: :: MSUALG_6:29
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s &amp; [x,y] in R . s9 &amp; a = t . x &amp; b = t . y ) )
proofend;

theorem Th30: :: MSUALG_6:30
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A holds InvCl R is stable
proofend;

Lm2: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_A_being_non-empty_MSAlgebra_over_S
for_R,_Q_being_ManySortedRelation_of_A_st_(_for_s_being_SortSymbol_of_S
for_a,_b_being_Element_of_A,s_holds_
(_[a,b]_in_Q_._s_iff_ex_s9_being_SortSymbol_of_S_ex_f_being_Function_of_(_the_Sorts_of_A_._s9),(_the_Sorts_of_A_._s)_ex_x,_y_being_Element_of_A,s9_st_
(_S2[f,s9,s]_&amp;_[x,y]_in_R_._s9_&amp;_a_=_f_._x_&amp;_b_=_f_._y_)_)_)_holds_
(_S1[Q]_&amp;_R_c=_Q_&amp;_(_for_P_being_ManySortedRelation_of_A_st_S1[P]_&amp;_R_c=_P_holds_
Q_c=_P_)_)
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ) holds
( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) )
let A be non-empty MSAlgebra over S; ::_thesis: for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ) holds
( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) )
let R, Q be ManySortedRelation of A; ::_thesis: ( ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ) implies ( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) ) )
defpred S1[ ManySortedRelation of A] means $1 is stable ;
defpred S2[ Function, SortSymbol of S, SortSymbol of S] means ( $2 = $3 &amp; ex h being Endomorphism of A st $1 = h . $2 );
A1: for s1, s2, s3 being SortSymbol of S
for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2)
for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] &amp; S2[f2,s2,s3] holds
S2[f2 * f1,s1,s3]
proof
let s1, s2, s3 be SortSymbol of S; ::_thesis: for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2)
for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] &amp; S2[f2,s2,s3] holds
S2[f2 * f1,s1,s3]
let f1 be Function of ( the Sorts of A . s1),( the Sorts of A . s2); ::_thesis: for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] &amp; S2[f2,s2,s3] holds
S2[f2 * f1,s1,s3]
let f2 be Function of ( the Sorts of A . s2),( the Sorts of A . s3); ::_thesis: ( S2[f1,s1,s2] &amp; S2[f2,s2,s3] implies S2[f2 * f1,s1,s3] )
assume A2: s1 = s2 ; ::_thesis: ( for h being Endomorphism of A holds not f1 = h . s1 or not S2[f2,s2,s3] or S2[f2 * f1,s1,s3] )
given h1 being Endomorphism of A such that A3: f1 = h1 . s1 ; ::_thesis: ( not S2[f2,s2,s3] or S2[f2 * f1,s1,s3] )
assume A4: s2 = s3 ; ::_thesis: ( for h being Endomorphism of A holds not f2 = h . s2 or S2[f2 * f1,s1,s3] )
given h2 being Endomorphism of A such that A5: f2 = h2 . s2 ; ::_thesis: S2[f2 * f1,s1,s3]
thus  s1 = s3 by A2, A4; ::_thesis: ex h being Endomorphism of A st f2 * f1 = h . s1
reconsider h = h2 ** h1 as Endomorphism of A ;
take  h ; ::_thesis: f2 * f1 = h . s1
thus  f2 * f1 = h . s1 by A2, A3, A5, MSUALG_3:2; ::_thesis: verum
end;
A6: for R being ManySortedRelation of A holds
( S1[R] iff for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
proof
let R be ManySortedRelation of A; ::_thesis: ( S1[R] iff for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
thus  ( R is stable implies for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st s1 = s2 &amp; ex h being Endomorphism of A st f = h . s1 holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) by Def9; ::_thesis: ( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] )
assume A7: for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ; ::_thesis: S1[R]
thus  R is stable ::_thesis: verum
proof
let h be Endomorphism of A; :: according toMSUALG_6:def_9 ::_thesis: for s being SortSymbol of S
for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s
let s be SortSymbol of S; ::_thesis: for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s
thus  for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s by A7; ::_thesis: verum
end;
end;
A8: for s being SortSymbol of S holds S2[ id ( the Sorts of A . s),s,s]
proof
reconsider h = id the Sorts of A as Endomorphism of A by Th4;
let s be SortSymbol of S; ::_thesis: S2[ id ( the Sorts of A . s),s,s]
thus  s = s ; ::_thesis: ex h being Endomorphism of A st id ( the Sorts of A . s) = h . s
take  h ; ::_thesis: id ( the Sorts of A . s) = h . s
thus  id ( the Sorts of A . s) = h . s by MSUALG_3:def_1; ::_thesis: verum
end;
assume A9: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] &amp; [x,y] in R . s9 &amp; a = f . x &amp; b = f . y ) ) ; ::_thesis: ( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) )
thus  ( S1[Q] &amp; R c= Q &amp; ( for P being ManySortedRelation of A st S1[P] &amp; R c= P holds
Q c= P ) ) from MSUALG_6:sch_4(A6, A1, A8, A9); ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be ManySortedRelation of the Sorts of A;
func StabCl R ->  stable ManySortedRelation of A means :Def12: :: MSUALG_6:def 12
( R c= it &amp; ( for Q being stable ManySortedRelation of A st R c= Q holds
it c= Q ) );
uniqueness
 for b1, b2 being stable ManySortedRelation of A st R c= b1 &amp; ( for Q being stable ManySortedRelation of A st R c= Q holds
b1 c= Q ) &amp; R c= b2 &amp; ( for Q being stable ManySortedRelation of A st R c= Q holds
b2 c= Q ) holds
b1 = b2
proofend;
existence
 ex b1 being stable ManySortedRelation of A st
( R c= b1 &amp; ( for Q being stable ManySortedRelation of A st R c= Q holds
b1 c= Q ) )
proofend;
end;

:: deftheorem Def12 defines StabCl MSUALG_6:def_12_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for b4 being stable ManySortedRelation of A holds
( b4 = StabCl R iff ( R c= b4 &amp; ( for Q being stable ManySortedRelation of A st R c= Q holds
b4 c= Q ) ) );

theorem Th31: :: MSUALG_6:31
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in R . s &amp; a = (h . s) . x &amp; b = (h . s) . y ) )
proofend;

theorem :: MSUALG_6:32
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) is stable by Th30;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be ManySortedRelation of the Sorts of A;
func TRS R ->  invariant stable ManySortedRelation of A means :Def13: :: MSUALG_6:def 13
( R c= it &amp; ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
it c= Q ) );
uniqueness
 for b1, b2 being invariant stable ManySortedRelation of A st R c= b1 &amp; ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b1 c= Q ) &amp; R c= b2 &amp; ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b2 c= Q ) holds
b1 = b2
proofend;
existence
 ex b1 being invariant stable ManySortedRelation of A st
( R c= b1 &amp; ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b1 c= Q ) )
proofend;
end;

:: deftheorem Def13 defines TRS MSUALG_6:def_13_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for b4 being invariant stable ManySortedRelation of A holds
( b4 = TRS R iff ( R c= b4 &amp; ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b4 c= Q ) ) );

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be V16() ManySortedRelation of A;
cluster InvCl R -> V16() invariant ;
coherence
 InvCl R is non-empty
proofend;
cluster StabCl R -> V16() stable ;
coherence
 StabCl R is non-empty
proofend;
cluster TRS R -> V16() invariant stable ;
coherence
 TRS R is non-empty
proofend;
end;

theorem :: MSUALG_6:33
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being invariant ManySortedRelation of A holds InvCl R = R
proofend;

theorem :: MSUALG_6:34
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A holds StabCl R = R
proofend;

theorem :: MSUALG_6:35
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being invariant stable ManySortedRelation of A holds TRS R = R
proofend;

theorem :: MSUALG_6:36
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A holds
( StabCl R c= TRS R &amp; InvCl R c= TRS R &amp; StabCl (InvCl R) c= TRS R )
proofend;

theorem Th37: :: MSUALG_6:37
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R
proofend;

theorem :: MSUALG_6:38
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s &amp; ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 &amp; a = t . ((h . s9) . l) &amp; b = t . ((h . s9) . r) ) ) )
proofend;

begin

theorem Th39: :: MSUALG_6:39
for A being set
for R, E being Relation of A st ( for a, b being set st a in A &amp; b in A holds
( [a,b] in E iff a,b are_convertible_wrt R ) ) holds
( E is total &amp; E is symmetric &amp; E is transitive )
proofend;

theorem Th40: :: MSUALG_6:40
for A being set
for R being Relation of A
for E being Equivalence_Relation of A st R c= E holds
for a, b being set st a in A &amp; a,b are_convertible_wrt R holds
[a,b] in E
proofend;

theorem Th41: :: MSUALG_6:41
for A being non empty set
for R being Relation of A
for a, b being Element of A holds
( [a,b] in EqCl R iff a,b are_convertible_wrt R )
proofend;

theorem Th42: :: MSUALG_6:42
for S being non empty set
for A being V16() ManySortedSet of S
for R being ManySortedRelation of A
for s being Element of S
for a, b being Element of A . s holds
( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
mode EquationalTheory of A is MSEquivalence-like invariant stable ManySortedRelation of A;
let R be ManySortedRelation of A;
func EqCl (R,A) ->  MSEquivalence-like ManySortedRelation of A equals :: MSUALG_6:def 14
 EqCl R;
coherence
 EqCl R is MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3;
end;

:: deftheorem  defines EqCl MSUALG_6:def_14_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds EqCl (R,A) = EqCl R;

theorem Th43: :: MSUALG_6:43
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds R c= EqCl (R,A)
proofend;

theorem Th44: :: MSUALG_6:44
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A
for E being MSEquivalence-like ManySortedRelation of A st R c= E holds
EqCl (R,A) c= E
proofend;

theorem Th45: :: MSUALG_6:45
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A
for s being SortSymbol of S
for a, b being Element of A,s st a,b are_convertible_wrt R . s holds
for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s
proofend;

theorem Th46: :: MSUALG_6:46
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A holds EqCl (R,A) is stable
proofend;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be stable ManySortedRelation of A;
cluster EqCl (R,A) ->  MSEquivalence-like stable ;
coherence
 EqCl (R,A) is stable by Th46;
end;

theorem Th47: :: MSUALG_6:47
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being invariant ManySortedRelation of A
for s1, s2 being SortSymbol of S
for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds
for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2
proofend;

theorem Th48: :: MSUALG_6:48
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant
proofend;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be invariant ManySortedRelation of A;
cluster EqCl (R,A) ->  MSEquivalence-like invariant ;
coherence
 EqCl (R,A) is invariant by Th48;
end;

theorem Th49: :: MSUALG_6:49
for S being non empty set
for A being V16() ManySortedSet of S
for R, E being ManySortedRelation of A st ( for s being Element of S
for a, b being Element of A . s holds
( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds
E is MSEquivalence_Relation-like
proofend;

theorem Th50: :: MSUALG_6:50
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R, E being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds
E is EquationalTheory of A
proofend;

theorem Th51: :: MSUALG_6:51
for S being non empty set
for A being V16() ManySortedSet of S
for R being ManySortedRelation of A
for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds
for s being Element of S
for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be ManySortedRelation of the Sorts of A;
func EqTh R ->  EquationalTheory of A means :Def15: :: MSUALG_6:def 15
( R c= it &amp; ( for Q being EquationalTheory of A st R c= Q holds
it c= Q ) );
uniqueness
 for b1, b2 being EquationalTheory of A st R c= b1 &amp; ( for Q being EquationalTheory of A st R c= Q holds
b1 c= Q ) &amp; R c= b2 &amp; ( for Q being EquationalTheory of A st R c= Q holds
b2 c= Q ) holds
b1 = b2
proofend;
existence
 ex b1 being EquationalTheory of A st
( R c= b1 &amp; ( for Q being EquationalTheory of A st R c= Q holds
b1 c= Q ) )
proofend;
end;

:: deftheorem Def15 defines EqTh MSUALG_6:def_15_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for b4 being EquationalTheory of A holds
( b4 = EqTh R iff ( R c= b4 &amp; ( for Q being EquationalTheory of A st R c= Q holds
b4 c= Q ) ) );

theorem :: MSUALG_6:52
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds
( EqCl (R,A) c= EqTh R &amp; InvCl R c= EqTh R &amp; StabCl R c= EqTh R &amp; TRS R c= EqTh R )
proofend;

theorem :: MSUALG_6:53
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s )
proofend;

theorem :: MSUALG_6:54
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)
proofend;