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

begin

definition

let S be non empty ManySortedSign ;
let A be MSAlgebra of S;
let s be SortSymbol of ;
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 func h2 ** h1 -> ManySortedFunction of A,A;
coherence
h2 ** h1 is ManySortedFunction of A,A

proof end;

end;

theorem Th1: :: MSUALG_6:1

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for o being OperSymbol of
for a being set st a in Args o,A holds
a is Function

proof end;

theorem Th2: :: MSUALG_6:2

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for o being OperSymbol of
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) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
attr A is feasible means :Def1: :: MSUALG_6:def 1
for o being OperSymbol of 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 of S holds
( A is feasible iff for o being OperSymbol of 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
for A being MSAlgebra of 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) <> {} )

proof end;

registration

let S be non empty non void ManySortedSign ;
cluster non-empty -> feasible MSAlgebra of S;
coherence
for b₁ being MSAlgebra of S st b₁ is non-empty holds
b₁ is feasible

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
cluster non-empty MSAlgebra of S;
existence
ex b₁ being MSAlgebra of S st b₁ is non-empty

proof end;

end;

definition

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

proof end;

end;

:: deftheorem Def2 defines Endomorphism MSUALG_6:def 2 :

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for b₃ being ManySortedFunction of ,A holds
( b₃ is Endomorphism of A iff b₃ is_homomorphism A,A );

theorem Th4: :: MSUALG_6:4

for S being non empty non void ManySortedSign
for A being MSAlgebra of S holds id the Sorts of A is Endomorphism of A

proof end;

theorem Th5: :: MSUALG_6:5

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for h1, h2 being ManySortedFunction of ,A
for o being OperSymbol of
for a being Element of Args o,A st a in Args o,A holds
h2 # (h1 # a) = (h2 ** h1) # a

proof end;

theorem Th6: :: MSUALG_6:6

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let h1, h2 be Endomorphism of A;
:: original: **
redefine func h2 ** 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 means :Def3: :: MSUALG_6:def 3
for s1, s2 being SortSymbol of holds
( [s1,s2] in it iff ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) );
existence
ex b₁ being Relation of st
for s1, s2 being SortSymbol of holds
( [s1,s2] in b₁ iff ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being Relation of st ( for s1, s2 being SortSymbol of holds
( [s1,s2] in b₁ iff ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ) & ( for s1, s2 being SortSymbol of holds
( [s1,s2] in b₂ iff ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def3 defines TranslationRel MSUALG_6:def 3 :

for S being non empty non void ManySortedSign
for b₂ being Relation of holds
( b₂ = TranslationRel S iff for s1, s2 being SortSymbol of holds
( [s1,s2] in b₂ iff ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) );

theorem Th7: :: MSUALG_6:7

for S being non empty non void ManySortedSign
for o being OperSymbol of
for A being MSAlgebra of 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

proof end;

theorem Th8: :: MSUALG_6:8

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra of S
for h being ManySortedFunction of ,A1
for o being OperSymbol of st Args o,A1 <> {} & 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)

proof end;

theorem Th9: :: MSUALG_6:9

for S being non empty non void ManySortedSign
for o being OperSymbol of
for i being Element of NAT st i in dom (the_arity_of o) holds
for A1, A2 being MSAlgebra of S
for h being ManySortedFunction of ,A1
for a, b being Element of Args o,A1 st a in Args o,A1 & h # a in Args o,A2 holds
for f, g1, g2 being Function st f = a & g1 = h # a & 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 & h # b = g1 +* i,(g2 . i) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let o be OperSymbol of ;
let i be Element of NAT ;
let A be MSAlgebra of 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) & ( 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 b₁ being Function st
( dom b₁ = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b₁ . x = (Den o,A) . (a +* i,x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b₁ . x = (Den o,A) . (a +* i,x) ) & dom b₂ = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b₂ . x = (Den o,A) . (a +* i,x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines transl MSUALG_6:def 4 :

for S being non empty non void ManySortedSign
for o being OperSymbol of
for i being Element of NAT
for A being MSAlgebra of S
for a, b₆ being Function holds
( b₆ = transl o,i,a,A iff ( dom b₆ = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b₆ . 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
for i being Element of NAT
for A being feasible MSAlgebra of 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)

proof end;

definition

let S be non empty non void ManySortedSign ;
let s1, s2 be SortSymbol of ;
let A be MSAlgebra of S;
let f be Function;
pred f is_e.translation_of A,s1,s2 means :Def5: :: MSUALG_6:def 5
ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args o,A & 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
for A being MSAlgebra of S
for f being Function holds
( f is_e.translation_of A,s1,s2 iff ex o being OperSymbol of st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args o,A & 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
for A being feasible MSAlgebra of 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 & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )

proof end;

theorem Th12: :: MSUALG_6:12

for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of
for A being MSAlgebra of S
for f being Function st f is_e.translation_of A,s1,s2 holds
[s1,s2] in TranslationRel S

proof end;

theorem :: MSUALG_6:13

for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of
for A being non-empty MSAlgebra of S st [s1,s2] in TranslationRel S holds
ex f being Function st f is_e.translation_of A,s1,s2

proof end;

theorem Th14: :: MSUALG_6:14

for S being non empty non void ManySortedSign
for A being feasible MSAlgebra of S
for s1, s2 being SortSymbol of
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of st i in dom p & f = p . i & s1 = q . i & 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 & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let s1, s2 be SortSymbol of ;
assume A1: 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) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) );
existence
ex b₁ 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
( b₁ = compose p,(the Sorts of A . s1) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) )

proof end;

end;

:: deftheorem Def6 defines Translation MSUALG_6:def 6 :

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s1, s2 being SortSymbol of st TranslationRel S reduces s1,s2 holds
for b₅ being Function of the Sorts of A . s1,the Sorts of A . s2 holds
( b₅ is Translation of A,s1,s2 iff ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( b₅ = compose p,(the Sorts of A . s1) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of st i in dom p & f = p . i & s1 = q . i & 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 of S
for s1, s2 being SortSymbol of 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 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of st i in dom p & f = p . i & s1 = q . i & 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

proof end;

theorem Th16: :: MSUALG_6:16

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s being SortSymbol of holds id (the Sorts of A . s) is Translation of A,s,s

proof end;

theorem Th17: :: MSUALG_6:17

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s1, s2 being SortSymbol of
for f being Function st f is_e.translation_of A,s1,s2 holds
( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )

proof end;

theorem Th18: :: MSUALG_6:18

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s1, s2, s3 being SortSymbol of st TranslationRel S reduces s1,s2 & 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

proof end;

theorem Th19: :: MSUALG_6:19

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s1, s2, s3 being SortSymbol of 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

proof end;

theorem :: MSUALG_6:20

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s1, s2, s3 being SortSymbol of 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

proof end;

scheme :: MSUALG_6:sch 1
TranslationInd{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), P₁[ set , set , set ] } :

for s1, s2 being SortSymbol of st TranslationRel F₁() reduces s1,s2 holds
for t being Translation of F₂(),s1,s2 holds P₁[t,s1,s2]

provided

A1: for s being SortSymbol of holds P₁[ id (the Sorts of F₂() . s),s,s] and
A2: for s1, s2, s3 being SortSymbol of st TranslationRel F₁() reduces s1,s2 holds
for t being Translation of F₂(),s1,s2 st P₁[t,s1,s2] holds
for f being Function st f is_e.translation_of F₂(),s2,s3 holds
P₁[f * t,s1,s3]

proof end;

theorem Th21: :: MSUALG_6:21

for S being non empty non void ManySortedSign
for A1, A2 being non-empty MSAlgebra of S
for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
for o being OperSymbol of
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))

proof end;

theorem :: MSUALG_6:22

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for h being Endomorphism of A
for o being OperSymbol of
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))

proof end;

theorem Th23: :: MSUALG_6:23

for S being non empty non void ManySortedSign
for A1, A2 being non-empty MSAlgebra of S
for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of
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 & T * (h . s1) = (h . s2) * t )

proof end;

theorem :: MSUALG_6:24

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for h being Endomorphism of A
for s1, s2 being SortSymbol of
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 & T * (h . s1) = (h . s2) * t )

proof end;

theorem Th25: :: MSUALG_6:25

for S being non empty non void ManySortedSign
for A1, A2 being non-empty MSAlgebra of S
for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of 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

proof end;

theorem Th26: :: MSUALG_6:26

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for h being Endomorphism of A
for s1, s2 being SortSymbol of 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

proof end;

begin

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let R be ManySortedRelation of A;
attr R is compatible means :Def7: :: MSUALG_6:def 7
for o being OperSymbol of
for a, b being Function st a in Args o,A & b in Args o,A & ( 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);
attr R is invariant means :Def8: :: MSUALG_6:def 8
for s1, s2 being SortSymbol of
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;
attr R is stable means :Def9: :: MSUALG_6:def 9
for h being Endomorphism of A
for s being SortSymbol of
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 of S
for R being ManySortedRelation of A holds
( R is compatible iff for o being OperSymbol of
for a, b being Function st a in Args o,A & b in Args o,A & ( 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 of S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of
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 of S
for R being ManySortedRelation of A holds
( R is stable iff for h being Endomorphism of A
for s being SortSymbol of
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 of S
for R being MSEquivalence-like ManySortedRelation of A holds
( R is compatible iff R is MSCongruence of A )

proof end;

theorem Th28: :: MSUALG_6:28

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of 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 )

proof end;

registration

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

proof end;

cluster MSEquivalence-like compatible -> MSEquivalence-like invariant ManySortedRelation of the Sorts of A,the Sorts of A;
coherence
for b₁ being MSEquivalence-like ManySortedRelation of A st b₁ is compatible holds
b₁ is invariant

proof end;

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{ F₁() -> non empty set , F₂() -> V5() ManySortedSet of , P₁[ set , set , set ] } :

ex R being ManySortedRelation of F₂() st
for i being Element of F₁()
for a, b being Element of F₂() . i holds
( [a,b] in R . i iff P₁[i,a,b] )

proof end;

scheme :: MSUALG_6:sch 3
MSRLambdaU{ F₁() -> set , F₂() -> ManySortedSet of F₁(), F₃( set ) -> set } :

( ex R being ManySortedRelation of F₂() st
for i being set st i in F₁() holds
R . i = F₃(i) & ( for R1, R2 being ManySortedRelation of F₂() st ( for i being set st i in F₁() holds
R1 . i = F₃(i) ) & ( for i being set st i in F₁() holds
R2 . i = F₃(i) ) holds
R1 = R2 ) )

provided

A1: for i being set st i in F₁() holds
F₃(i) is Relation of ,

proof end;

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 b₁ being ManySortedRelation of A st
for i being set st i in I holds
b₁ . i = id (A . i);
uniqueness
for b₁, b₂ being ManySortedRelation of A st ( for i being set st i in I holds
b₁ . i = id (A . i) ) & ( for i being set st i in I holds
b₂ . i = id (A . i) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def10 defines id MSUALG_6:def 10 :

for I being set
for A being ManySortedSet of I
for b₃ being ManySortedRelation of A holds
( b₃ = id I,A iff for i being set st i in I holds
b₃ . i = id (A . i) );

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
cluster MSEquivalence-like -> V5() ManySortedRelation of the Sorts of A,the Sorts of A;
coherence
for b₁ being ManySortedRelation of A st b₁ is MSEquivalence-like holds
b₁ is non-empty

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
cluster MSEquivalence-like invariant stable ManySortedRelation of the Sorts of A,the Sorts of A;
existence
ex b₁ being ManySortedRelation of A st
( b₁ is invariant & b₁ is stable & b₁ is MSEquivalence-like )

proof end;

end;

begin

scheme :: MSUALG_6:sch 4
MSRelCl{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), P₁[ set , set , set ], P₂[ set ], F₃() -> ManySortedRelation of F₂(), F₄() -> ManySortedRelation of F₂() } :

( P₂[F₄()] & F₃() c= F₄() & ( for P being ManySortedRelation of F₂() st P₂[P] & F₃() c= P holds
F₄() c= P ) )

provided

A1: for R being ManySortedRelation of F₂() holds
( P₂[R] iff for s1, s2 being SortSymbol of
for f being Function of the Sorts of F₂() . s1,the Sorts of F₂() . s2 st P₁[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
for f1 being Function of the Sorts of F₂() . s1,the Sorts of F₂() . s2
for f2 being Function of the Sorts of F₂() . s2,the Sorts of F₂() . s3 st P₁[f1,s1,s2] & P₁[f2,s2,s3] holds
P₁[f2 * f1,s1,s3] and
A3: for s being SortSymbol of holds P₁[ id (the Sorts of F₂() . s),s,s] and
A4: for s being SortSymbol of
for a, b being Element of F₂(),s holds
( [a,b] in F₄() . s iff ex s' being SortSymbol of ex f being Function of the Sorts of F₂() . s',the Sorts of F₂() . s ex x, y being Element of F₂(),s' st
( P₁[f,s',s] & [x,y] in F₃() . s' & a = f . x & b = f . y ) )

proof end;

Lm1: now

let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ) holds
( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) )
let A be non-empty MSAlgebra of S; :: thesis: for R, Q being ManySortedRelation of A st ( for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ) holds
( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) )
let R, Q be ManySortedRelation of A; :: thesis: ( ( for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ) implies ( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) ) )
defpred S₁[ ManySortedRelation of A] means $1 is invariant ;
defpred S₂[ Function, SortSymbol of , SortSymbol of ] means ( TranslationRel S reduces $2,$3 & $1 is Translation of A,$2,$3 );
assume A1: for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ; :: thesis: ( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) )
A2: for s being SortSymbol of holds S₂[ id (the Sorts of A . s),s,s] by Th16, REWRITE1:13;

A3: now

let R be ManySortedRelation of A; :: thesis: ( ( S₁[R] implies for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) & ( ( for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S₁[R] ) )
thus ( S₁[R] implies for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[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
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S₁[R] )
assume for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ; :: thesis: S₁[R]
then for s1, s2 being SortSymbol of 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 S₁[R] by Th28; :: thesis: verum

end;

A4: for s1, s2, s3 being SortSymbol of
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 S₂[f1,s1,s2] & S₂[f2,s2,s3] holds
S₂[f2 * f1,s1,s3] by Th18, REWRITE1:17;
thus ( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & 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 of 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 & ( for Q being invariant ManySortedRelation of A st R c= Q holds
it c= Q ) );
uniqueness
for b₁, b₂ being invariant ManySortedRelation of A st R c= b₁ & ( for Q being invariant ManySortedRelation of A st R c= Q holds
b₁ c= Q ) & R c= b₂ & ( for Q being invariant ManySortedRelation of A st R c= Q holds
b₂ c= Q ) holds
b₁ = b₂

proof end;

existence
ex b₁ being invariant ManySortedRelation of A st
( R c= b₁ & ( for Q being invariant ManySortedRelation of A st R c= Q holds
b₁ c= Q ) )

proof end;

end;

:: deftheorem Def11 defines InvCl MSUALG_6:def 11 :

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b₄ being invariant ManySortedRelation of A holds
( b₄ = InvCl R iff ( R c= b₄ & ( for Q being invariant ManySortedRelation of A st R c= Q holds
b₄ c= Q ) ) );

theorem Th29: :: MSUALG_6:29

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in (InvCl R) . s iff ex s' being SortSymbol of ex x, y being Element of A,s' ex t being Translation of A,s',s st
( TranslationRel S reduces s',s & [x,y] in R . s' & a = t . x & b = t . y ) )

proof end;

theorem Th30: :: MSUALG_6:30

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being stable ManySortedRelation of A holds InvCl R is stable

proof end;

Lm2: now

let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ) holds
( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) )
let A be non-empty MSAlgebra of S; :: thesis: for R, Q being ManySortedRelation of A st ( for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ) holds
( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) )
let R, Q be ManySortedRelation of A; :: thesis: ( ( for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ) implies ( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) ) )
defpred S₁[ ManySortedRelation of A] means $1 is stable ;
defpred S₂[ Function, SortSymbol of , SortSymbol of ] means ( $2 = $3 & ex h being Endomorphism of A st $1 = h . $2 );
A1: for s1, s2, s3 being SortSymbol of
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 S₂[f1,s1,s2] & S₂[f2,s2,s3] holds
S₂[f2 * f1,s1,s3]

proof

let s1, s2, s3 be SortSymbol of ; :: 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 S₂[f1,s1,s2] & S₂[f2,s2,s3] holds
S₂[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 S₂[f1,s1,s2] & S₂[f2,s2,s3] holds
S₂[f2 * f1,s1,s3]
let f2 be Function of the Sorts of A . s2,the Sorts of A . s3; :: thesis: ( S₂[f1,s1,s2] & S₂[f2,s2,s3] implies S₂[f2 * f1,s1,s3] )
assume A2: s1 = s2 ; :: thesis: ( for h being Endomorphism of A holds not f1 = h . s1 or not S₂[f2,s2,s3] or S₂[f2 * f1,s1,s3] )
given h1 being Endomorphism of A such that A3: f1 = h1 . s1 ; :: thesis: ( not S₂[f2,s2,s3] or S₂[f2 * f1,s1,s3] )
assume A4: s2 = s3 ; :: thesis: ( for h being Endomorphism of A holds not f2 = h . s2 or S₂[f2 * f1,s1,s3] )
given h2 being Endomorphism of A such that A5: f2 = h2 . s2 ; :: thesis: S₂[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
( S₁[R] iff for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[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: ( S₁[R] iff for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[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
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st s1 = s2 & 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
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S₁[R] )
assume A7: for s1, s2 being SortSymbol of
for f being Function of the Sorts of A . s1,the Sorts of A . s2 st S₂[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ; :: thesis: S₁[R]
thus R is stable :: thesis: verum

proof

let h be Endomorphism of A; :: according to MSUALG_6:def 9 :: thesis: for s being SortSymbol of
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 ; :: 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 holds S₂[ 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 ; :: thesis: S₂[ 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
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( S₂[f,s',s] & [x,y] in R . s' & a = f . x & b = f . y ) ) ; :: thesis: ( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & R c= P holds
Q c= P ) )
thus ( S₁[Q] & R c= Q & ( for P being ManySortedRelation of A st S₁[P] & 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 of 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 & ( for Q being stable ManySortedRelation of A st R c= Q holds
it c= Q ) );
uniqueness
for b₁, b₂ being stable ManySortedRelation of A st R c= b₁ & ( for Q being stable ManySortedRelation of A st R c= Q holds
b₁ c= Q ) & R c= b₂ & ( for Q being stable ManySortedRelation of A st R c= Q holds
b₂ c= Q ) holds
b₁ = b₂

proof end;

existence
ex b₁ being stable ManySortedRelation of A st
( R c= b₁ & ( for Q being stable ManySortedRelation of A st R c= Q holds
b₁ c= Q ) )

proof end;

end;

:: deftheorem Def12 defines StabCl MSUALG_6:def 12 :

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b₄ being stable ManySortedRelation of A holds
( b₄ = StabCl R iff ( R c= b₄ & ( for Q being stable ManySortedRelation of A st R c= Q holds
b₄ c= Q ) ) );

theorem Th31: :: MSUALG_6:31

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of
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 & a = (h . s) . x & b = (h . s) . y ) )

proof end;

theorem :: MSUALG_6:32

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 of 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 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
it c= Q ) );
uniqueness
for b₁, b₂ being invariant stable ManySortedRelation of A st R c= b₁ & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b₁ c= Q ) & R c= b₂ & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b₂ c= Q ) holds
b₁ = b₂

proof end;

existence
ex b₁ being invariant stable ManySortedRelation of A st
( R c= b₁ & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b₁ c= Q ) )

proof end;

end;

:: deftheorem Def13 defines TRS MSUALG_6:def 13 :

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b₄ being invariant stable ManySortedRelation of A holds
( b₄ = TRS R iff ( R c= b₄ & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b₄ c= Q ) ) );

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let R be V5() ManySortedRelation of A;
cluster InvCl R -> V5() invariant ;
coherence
InvCl R is non-empty

proof end;

cluster StabCl R -> V5() stable ;
coherence
StabCl R is non-empty

proof end;

cluster TRS R -> V5() invariant stable ;
coherence
TRS R is non-empty

proof end;

end;

theorem :: MSUALG_6:33

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being invariant ManySortedRelation of A holds InvCl R = R

proof end;

theorem :: MSUALG_6:34

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being stable ManySortedRelation of A holds StabCl R = R

proof end;

theorem :: MSUALG_6:35

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being invariant stable ManySortedRelation of A holds TRS R = R

proof end;

theorem :: MSUALG_6:36

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A holds
( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )

proof end;

theorem Th37: :: MSUALG_6:37

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R

proof end;

theorem :: MSUALG_6:38

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

proof end;

begin

theorem Th39: :: MSUALG_6:39

for A being set
for R, E being Relation of st ( for a, b being set st a in A & b in A holds
( [a,b] in E iff a,b are_convertible_wrt R ) ) holds
( E is total & E is symmetric & E is transitive )

proof end;

theorem Th40: :: MSUALG_6:40

for A being set
for R being Relation of
for E being Equivalence_Relation of st R c= E holds
for a, b being set st a in A & a,b are_convertible_wrt R holds
[a,b] in E

proof end;

theorem Th41: :: MSUALG_6:41

for A being non empty set
for R being Relation of
for a, b being Element of A holds
( [a,b] in EqCl R iff a,b are_convertible_wrt R )

proof end;

theorem Th42: :: MSUALG_6:42

for S being non empty set
for A being V5() ManySortedSet of
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 )

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of 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 5;

end;

:: deftheorem defines EqCl MSUALG_6:def 14 :

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 of S
for R being ManySortedRelation of A holds R c= EqCl R,A

proof end;

theorem Th44: :: MSUALG_6:44

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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

proof end;

theorem Th45: :: MSUALG_6:45

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being stable ManySortedRelation of A
for s being SortSymbol of
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

proof end;

theorem Th46: :: MSUALG_6:46

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being stable ManySortedRelation of A holds EqCl R,A is stable

proof end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of 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 of S
for R being invariant ManySortedRelation of A
for s1, s2 being SortSymbol of
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

proof end;

theorem Th48: :: MSUALG_6:48

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being invariant ManySortedRelation of A holds EqCl R,A is invariant

proof end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of 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 V5() ManySortedSet of
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

proof end;

theorem Th50: :: MSUALG_6:50

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R, E being ManySortedRelation of A st ( for s being SortSymbol of
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

proof end;

theorem Th51: :: MSUALG_6:51

for S being non empty set
for A being V5() ManySortedSet of
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

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of 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 & ( for Q being EquationalTheory of A st R c= Q holds
it c= Q ) );
uniqueness
for b₁, b₂ being EquationalTheory of A st R c= b₁ & ( for Q being EquationalTheory of A st R c= Q holds
b₁ c= Q ) & R c= b₂ & ( for Q being EquationalTheory of A st R c= Q holds
b₂ c= Q ) holds
b₁ = b₂

proof end;

existence
ex b₁ being EquationalTheory of A st
( R c= b₁ & ( for Q being EquationalTheory of A st R c= Q holds
b₁ c= Q ) )

proof end;

end;

:: deftheorem Def15 defines EqTh MSUALG_6:def 15 :

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b₄ being EquationalTheory of A holds
( b₄ = EqTh R iff ( R c= b₄ & ( for Q being EquationalTheory of A st R c= Q holds
b₄ c= Q ) ) );

theorem :: MSUALG_6:52

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A holds
( EqCl R,A c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )

proof end;

theorem :: MSUALG_6:53

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

proof end;

theorem :: MSUALG_6:54

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A holds EqTh R = EqCl (TRS R),A

proof end;