:: Translations, Endomorphisms, and Stable Equational Theories
:: by Grzegorz Bancerek
::
:: Received February 9, 1996
:: Copyright (c) 1996-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, MSUALG_1, SUBSET_1, FUNCT_1, PBOOLE, MEMBER_1,
RELAT_1, STRUCT_0, CARD_3, MARGREL1, PARTFUN1, MOD_4, MSUALG_3, NAT_1,
FUNCT_4, RLTOPSP1, TARSKI, REWRITE1, FUNCOP_1, FINSEQ_1, ARYTM_3,
FUNCT_7, CARD_1, XXREAL_0, ORDINAL4, MSUALG_4, CIRCUIT2, MCART_1,
ZFMISC_1, EQREL_1, RELAT_2, MSUALG_5, MSUALG_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, XTUPLE_0, MCART_1, STRUCT_0, RELAT_1, RELAT_2, RELSET_1, EQREL_1,
REWRITE1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, FINSEQ_1, CARD_3, FUNCOP_1,
MSUALG_1, MSUALG_3, MSUALG_4, MSUALG_5, FUNCT_7, XXREAL_0;
constructors NAT_1, NAT_D, REWRITE1, FUNCT_7, MSUALG_3, MSUALG_5, RELSET_1,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1,
XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, PBOOLE, REWRITE1, FUNCT_7, STRUCT_0,
MSUALG_1, MSUALG_3, MSUALG_4, MSUALG_5, ORDINAL1, CARD_1, RELSET_1,
XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Endomorphisms and translations
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;
redefine func h2**h1 -> ManySortedFunction of A,A;
end;
theorem :: MSUALG_6:1
for S being non empty non void ManySortedSign for A being
MSAlgebra over S for o being OperSymbol of S, a being set st a in Args(o,A)
holds a is Function;
theorem :: MSUALG_6:2
for S being non empty non void ManySortedSign for A being
MSAlgebra over S for o being OperSymbol of S, 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);
definition
let S be non empty non void ManySortedSign;
let A be MSAlgebra over S;
attr A is feasible means
:: MSUALG_6:def 1
for o being OperSymbol of S st Args(o,A) <> {} holds Result(o,A) <> {};
end;
theorem :: 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) <> {};
registration
let S be non empty non void ManySortedSign;
cluster non-empty -> feasible for MSAlgebra over S;
end;
registration
let S be non empty non void ManySortedSign;
cluster non-empty for MSAlgebra over S;
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
:: MSUALG_6:def 2
it is_homomorphism A,A;
end;
reserve S for non empty non void ManySortedSign,
A for MSAlgebra over S;
theorem :: MSUALG_6:4
id the Sorts of A is Endomorphism of A;
theorem :: MSUALG_6:5
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;
theorem :: MSUALG_6:6
for h1,h2 being Endomorphism of A holds h2**h1 is Endomorphism of A;
definition
let S be non empty non void ManySortedSign;
let A be MSAlgebra over S;
let h1,h2 be Endomorphism of A;
redefine func h2**h1 -> Endomorphism of A;
end;
definition
let S be non empty non void ManySortedSign;
func TranslationRel S -> Relation of the carrier of S means
:: 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 & ex i being Element of NAT st i in dom the_arity_of
o & (the_arity_of o)/.i = s1;
end;
theorem :: MSUALG_6:7
for S being non empty non void ManySortedSign, o being OperSymbol
of S for A being MSAlgebra over S, a being Function st a in Args(o,A)
for i being Nat, x being Element of A,(the_arity_of o)/.i holds a+*(i,x)
in Args(o,A);
theorem :: MSUALG_6:8
for A1,A2 being MSAlgebra over S, h being ManySortedFunction of
A1,A2 for o being OperSymbol of S st Args(o,A1) <> {} & Args(o,A2) <> {} for i
being Element of NAT st i in dom the_arity_of o 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);
theorem :: MSUALG_6:9
for S being non empty non void ManySortedSign, o being OperSymbol
of S for i being Element of NAT st i in dom the_arity_of o 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) & h#a in Args(o,A2) for f,g1,g2 being Function
st f = a & g1 = h#a & g2 = h#b 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);
definition
let S be non empty non void ManySortedSign, o be OperSymbol of S;
let i be Nat;
let A be MSAlgebra over S;
let a be Function;
func transl(o,i,a,A) -> Function means
:: MSUALG_6:def 4
dom it = (the Sorts of A).((the_arity_of o)/.i) &
for x being object st x in (the Sorts of A).((the_arity_of o
)/.i) holds it.x = Den(o,A).(a+*(i,x));
end;
theorem :: MSUALG_6:10
for S being non empty non void ManySortedSign, o being
OperSymbol of S for i being Element of NAT for A being feasible MSAlgebra over
S, 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;
definition
let S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S;
let A be MSAlgebra over S;
let f be Function;
pred f is_e.translation_of A,s1,s2 means
:: MSUALG_6:def 5
ex o being OperSymbol of S
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;
theorem :: MSUALG_6:11
for S being non empty non void ManySortedSign, s1,s2 being
SortSymbol of S for A being feasible MSAlgebra over S, 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 <> {};
theorem :: MSUALG_6:12
for S being non empty non void ManySortedSign, s1,s2 being
SortSymbol of S for A being MSAlgebra over S, f being Function st f
is_e.translation_of A,s1,s2 holds [s1,s2] in TranslationRel S;
theorem :: MSUALG_6:13
for S being non empty non void ManySortedSign, s1,s2 being SortSymbol
of S for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S ex f
being Function st f is_e.translation_of A,s1,s2;
theorem :: 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, p being Function-yielding FinSequence st len q
= len p+1 & s1 = q.1 & s2 = q.len q & for i being (Element of NAT), f being
Function, s1,s2 being SortSymbol of S 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 <> {});
definition
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let s1,s2 be SortSymbol of S such that
TranslationRel S reduces s1,s2;
mode Translation of A,s1,s2 -> Function of (the Sorts of A).s1,(the Sorts of
A).s2 means
:: MSUALG_6:def 6
ex q being RedSequence of TranslationRel S, 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), f being
Function, s1,s2 being SortSymbol of S st i in dom p & f = p.i & s1 = q.i & s2 =
q.(i+1) holds f is_e.translation_of A,s1,s2;
end;
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 for q being RedSequence of TranslationRel S, p being Function-yielding
FinSequence st len q = len p+1 & s1 = q.1 & s2 = q.len q & for i being (Element
of NAT), f being Function, s1,s2 being SortSymbol of S 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;
reserve A for non-empty MSAlgebra over S;
theorem :: MSUALG_6:16
for s being SortSymbol of S holds id ((the Sorts of A).s) is
Translation of A,s,s;
theorem :: MSUALG_6:17
for s1,s2 being SortSymbol of S, 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;
theorem :: MSUALG_6:18
for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces
s1,s2 & TranslationRel S reduces s2,s3 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;
theorem :: MSUALG_6:19
for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces
s1,s2 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;
theorem :: MSUALG_6:20
for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces s2,s3
for f being Function st f is_e.translation_of A,s1,s2 for t being Translation
of A,s2,s3 holds t*f is Translation of A,s1,s3;
scheme :: MSUALG_6:sch 1
TranslationInd {S() -> non empty non void ManySortedSign, A() -> non-empty
MSAlgebra over S(), P[set,set,set]}: for s1,s2 being SortSymbol of S() st
TranslationRel S() reduces s1,s2 for t being Translation of A(),s1,s2 holds P[t
,s1,s2]
provided
for s being SortSymbol of S() holds P[id ((the Sorts of A()).s),s,s] and
for s1,s2,s3 being SortSymbol of S() st TranslationRel S() reduces
s1,s2 for t being Translation of A(),s1,s2 st P[t,s1,s2] for f being Function
st f is_e.translation_of A(),s2,s3 holds P[f*t,s1,s3];
theorem :: MSUALG_6:21
for A1,A2 being non-empty MSAlgebra over S for h being
ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for o being OperSymbol
of S, i being Element of NAT st i in dom the_arity_of o 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));
theorem :: MSUALG_6:22
for h being Endomorphism of A for o being OperSymbol of S, i being
Element of NAT st i in dom the_arity_of o 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));
theorem :: MSUALG_6:23
for A1,A2 being non-empty MSAlgebra over S for h being
ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for s1,s2 being
SortSymbol of S, t being Function st t is_e.translation_of A1,s1,s2 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;
theorem :: MSUALG_6:24
for h being Endomorphism of A for s1,s2 being SortSymbol of S, t being
Function st t is_e.translation_of A,s1,s2 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;
theorem :: MSUALG_6:25
for A1,A2 being non-empty MSAlgebra over S for h being
ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for s1,s2 being
SortSymbol of S st TranslationRel S reduces s1,s2 for t being Translation of A1
,s1,s2 ex T being Translation of A2,s1,s2 st T*(h.s1) = (h.s2)*t;
theorem :: MSUALG_6:26
for h being Endomorphism of A for s1,s2 being SortSymbol of S st
TranslationRel S reduces s1,s2 for t being Translation of A,s1,s2 ex T being
Translation of A,s1,s2 st T*(h.s1) = (h.s2)*t;
begin :: Compatibility, invariantness, and stability
definition
let S be non empty non void ManySortedSign;
let A be MSAlgebra over S;
let R be ManySortedRelation of A;
attr R is compatible means
:: MSUALG_6:def 7
for o being OperSymbol of S, a,b being
Function st a in Args(o,A) & b in Args(o,A) & (for n be 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
:: MSUALG_6:def 8
for s1,s2 being SortSymbol of S for t
being Function st t is_e.translation_of A,s1,s2 for a,b being set st [a,b] in R
.s1 holds [t.a, t.b] in R.s2;
attr R is stable means
:: 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;
theorem :: MSUALG_6:27
for R being MSEquivalence-like ManySortedRelation of A holds R is
compatible iff R is MSCongruence of A;
theorem :: MSUALG_6:28
for R being ManySortedRelation of A holds R is invariant iff for
s1,s2 being SortSymbol of S st TranslationRel S reduces s1,s2 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;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
cluster invariant -> compatible for
MSEquivalence-like ManySortedRelation of A;
cluster compatible -> invariant for
MSEquivalence-like ManySortedRelation of A;
end;
registration
let X be non empty set;
cluster id X -> non empty;
end;
scheme :: MSUALG_6:sch 2
MSRExistence {I() -> non empty set, A() -> non-empty ManySortedSet of I(),
P[object,object,object]}:
ex R being ManySortedRelation of A() st for i being Element of
I() for a,b being Element of A().i holds [a,b] in R.i iff P[i,a,b];
scheme :: MSUALG_6:sch 3
MSRLambdaU{I() -> set, A() -> ManySortedSet of I(), F(object) -> set}:
(ex R
being ManySortedRelation of A() st
for i being object st i in I() holds R.i = F(i)
) & for R1,R2 being ManySortedRelation of A() st
(for i being object st i in I()
holds R1.i = F(i)) &
(for i being object st i in I() holds R2.i = F(i)) holds R1 =
R2
provided
for i being set st i in I() holds F(i) is Relation of A().i, A().i;
definition
let I be set, A be ManySortedSet of I;
func id(I,A) -> ManySortedRelation of A means
:: MSUALG_6:def 10
for i being object st i in I holds it.i = id (A.i);
end;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
cluster MSEquivalence-like -> non-empty for ManySortedRelation of A;
end;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
cluster invariant stable MSEquivalence-like for ManySortedRelation of A;
end;
begin :: Invariant, stable, and invariant stable closure
reserve S for non empty non void ManySortedSign,
A for non-empty MSAlgebra over S,
R for ManySortedRelation of the Sorts of A;
scheme :: MSUALG_6:sch 4
MSRelCl {S() -> non empty non void ManySortedSign, A() -> non-empty
MSAlgebra over S(), P[set,set,set], R[set], R,Q() -> ManySortedRelation of A()}
: R[Q()] & R() c= Q() & for P being ManySortedRelation of A() st R[P] & R() c=
P holds Q() c= P
provided
for R being ManySortedRelation of A() holds R[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 P[f,s1,s2] for a,b being set st [a,b] in R.s1 holds [f.a,f.b] in R.s2
and
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 P[f1,s1,s2] & P[f2,s2,s3] holds P[f2*f1,s1,s3]
and
for s being SortSymbol of S() holds P[id ((the Sorts of A()).s),s,s] and
for s being SortSymbol of S(), a,b being Element of A(),s holds [a,b
] in Q().s iff ex s9 being SortSymbol of S(), f being Function of (the Sorts of
A()).s9,(the Sorts of A()).s, x,y being Element of A(),s9 st P[f,s9,s] & [x,y]
in R().s9 & a = f.x & b = f.y;
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
:: MSUALG_6:def 11
R c= it &
for Q being invariant ManySortedRelation of A st R c= Q holds it c= Q;
end;
theorem :: MSUALG_6:29
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, x,y being Element of A,s9 st ex t being Translation
of A,s9,s st TranslationRel S reduces s9,s & [x,y] in R.s9 & a = t.x & b = t.y;
theorem :: MSUALG_6:30
for R being stable ManySortedRelation of A holds InvCl R is stable;
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
:: MSUALG_6:def 12
R c= it & for Q being stable ManySortedRelation of A st R c= Q holds it c= Q;
end;
theorem :: MSUALG_6:31
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, h being Endomorphism of A st [x,y] in R.s & a = h.s.x
& b = h.s.y;
theorem :: MSUALG_6:32
InvCl StabCl R is stable;
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
:: MSUALG_6:def 13
R c=
it & for Q being invariant stable ManySortedRelation of A st R c= Q holds it c=
Q;
end;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let R be non-empty ManySortedRelation of A;
cluster InvCl R -> non-empty;
cluster StabCl R -> non-empty;
cluster TRS R -> non-empty;
end;
theorem :: MSUALG_6:33
for R being invariant ManySortedRelation of A holds InvCl R = R;
theorem :: MSUALG_6:34
for R being stable ManySortedRelation of A holds StabCl R = R;
theorem :: MSUALG_6:35
for R being invariant stable ManySortedRelation of A holds TRS R = R;
theorem :: MSUALG_6:36
StabCl R c= TRS R & InvCl R c= TRS R & StabCl InvCl R c= TRS R;
theorem :: MSUALG_6:37
InvCl StabCl R = TRS R;
theorem :: MSUALG_6:38
for R being ManySortedRelation of the Sorts of A for s being
SortSymbol of S, 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 & ex l,r being Element
of A,s9, h being Endomorphism of A, t being Translation of A, s9, s st [l,r] in
R.s9 & a = t.(h.s9.l) & b = t.(h.s9.r);
begin :: Equational theory
theorem :: MSUALG_6:39
for A being set for R,E being Relation of A 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 symmetric transitive;
theorem :: MSUALG_6:40
for A being set, R being Relation of A for E being
Equivalence_Relation of A st R c= E for a,b being object st a in A & a,b
are_convertible_wrt R holds [a,b] in E;
theorem :: MSUALG_6:41
for A being non empty set, 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;
theorem :: MSUALG_6:42
for S being non empty set, A being non-empty 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;
definition
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
mode EquationalTheory of A is stable invariant MSEquivalence-like
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;
end;
theorem :: MSUALG_6:43
for R being ManySortedRelation of A holds R c= EqCl(R,A);
theorem :: MSUALG_6:44
for R being ManySortedRelation of A for E being
MSEquivalence-like ManySortedRelation of A st R c= E holds EqCl(R,A) c= E;
theorem :: MSUALG_6:45
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 for
h being Endomorphism of A holds h.s.a, h.s.b are_convertible_wrt R.s;
theorem :: MSUALG_6:46
for R being stable ManySortedRelation of A holds EqCl(R,A) is stable;
registration
let S,A;
let R be stable ManySortedRelation of A;
cluster EqCl(R,A) -> stable;
end;
theorem :: MSUALG_6:47
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
for t being Function st t is_e.translation_of A,s1,s2 holds t.a, t.b
are_convertible_wrt R.s2;
theorem :: MSUALG_6:48
for R being invariant ManySortedRelation of A holds EqCl(R,A) is invariant;
registration
let S,A;
let R be invariant ManySortedRelation of A;
cluster EqCl(R,A) -> invariant;
end;
theorem :: MSUALG_6:49
for S being non empty set, A being non-empty 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;
theorem :: MSUALG_6:50
for R,E being ManySortedRelation of A st for s being SortSymbol
of S, 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;
theorem :: MSUALG_6:51
for S being non empty set, A being non-empty ManySortedSet of S
for R being ManySortedRelation of A for E being MSEquivalence_Relation-like
ManySortedRelation of A st R c= E 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;
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
:: MSUALG_6:def 15
R c= it & for Q being EquationalTheory of A st R c= Q holds it c= Q;
end;
theorem :: MSUALG_6:52
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;
theorem :: MSUALG_6:53
for R being ManySortedRelation of A for s being SortSymbol of S, a,b
being Element of A,s holds [a,b] in (EqTh R).s iff a,b are_convertible_wrt (TRS
R).s;
theorem :: MSUALG_6:54
for R being ManySortedRelation of A holds EqTh R = EqCl(TRS R,A);