let S be 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
let A be 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
let R, E be ManySortedRelation of A; ( ( 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 ) ) implies E is EquationalTheory of A )
assume A1:
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 )
; E is EquationalTheory of A
A2:
E is stable
proof
let h be
Endomorphism of
A;
MSUALG_6:def 9 for s being SortSymbol of S
for a, b being set st [a,b] in E . s holds
[((h . s) . a),((h . s) . b)] in E . slet s be
SortSymbol of
S;
for a, b being set st [a,b] in E . s holds
[((h . s) . a),((h . s) . b)] in E . slet a,
b be
set ;
( [a,b] in E . s implies [((h . s) . a),((h . s) . b)] in E . s )
assume A3:
[a,b] in E . s
;
[((h . s) . a),((h . s) . b)] in E . s
then reconsider x =
a,
y =
b as
Element of
A,
s by ZFMISC_1:87;
reconsider a9 =
(h . s) . x,
b9 =
(h . s) . y as
Element of
A,
s ;
x,
y are_convertible_wrt (TRS R) . s
by A1, A3;
then
a9,
b9 are_convertible_wrt (TRS R) . s
by Th45;
hence
[((h . s) . a),((h . s) . b)] in E . s
by A1;
verum
end;
A4:
E is invariant
proof
let s1,
s2 be
SortSymbol of
S;
MSUALG_6:def 8 for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in E . s1 holds
[(t . a),(t . b)] in E . s2let t be
Function;
( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in E . s1 holds
[(t . a),(t . b)] in E . s2 )
assume A5:
t is_e.translation_of A,
s1,
s2
;
for a, b being set st [a,b] in E . s1 holds
[(t . a),(t . b)] in E . s2
then reconsider f =
t as
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) by Th11;
let a,
b be
set ;
( [a,b] in E . s1 implies [(t . a),(t . b)] in E . s2 )
assume A6:
[a,b] in E . s1
;
[(t . a),(t . b)] in E . s2
then reconsider x =
a,
y =
b as
Element of
A,
s1 by ZFMISC_1:87;
x,
y are_convertible_wrt (TRS R) . s1
by A1, A6;
then A7:
t . x,
t . y are_convertible_wrt (TRS R) . s2
by A5, Th47;
A8:
t . y = f . y
;
t . x = f . x
;
hence
[(t . a),(t . b)] in E . s2
by A1, A8, A7;
verum
end;
E is MSEquivalence_Relation-like
by A1, Th49;
hence
E is EquationalTheory of A
by A2, A4, MSUALG_4:def 3; verum