let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of S; :: thesis: 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; :: thesis: ( ( 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 )
; :: thesis: E is EquationalTheory of A
then A2:
E is MSEquivalence_Relation-like
by Th49;
A3:
E is stable
proof
let h be
Endomorphism of
A;
:: according to MSUALG_6:def 9 :: thesis: 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;
:: thesis: 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 ;
:: thesis: ( [a,b] in E . s implies [((h . s) . a),((h . s) . b)] in E . s )
assume A4:
[a,b] in E . s
;
:: thesis: [((h . s) . a),((h . s) . b)] in E . s
then reconsider x =
a,
y =
b as
Element of
A,
s by ZFMISC_1:106;
reconsider a' =
(h . s) . x,
b' =
(h . s) . y as
Element of
A,
s ;
x,
y are_convertible_wrt (TRS R) . s
by A1, A4;
then
a',
b' are_convertible_wrt (TRS R) . s
by Th45;
hence
[((h . s) . a),((h . s) . b)] in E . s
by A1;
:: thesis: verum
end;
E is invariant
proof
let s1,
s2 be
SortSymbol of
S;
:: according to MSUALG_6:def 8 :: thesis: 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;
:: thesis: ( 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
;
:: thesis: 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 ;
:: thesis: ( [a,b] in E . s1 implies [(t . a),(t . b)] in E . s2 )
assume A6:
[a,b] in E . s1
;
:: thesis: [(t . a),(t . b)] in E . s2
then reconsider x =
a,
y =
b as
Element of
A,
s1 by ZFMISC_1:106;
x,
y are_convertible_wrt (TRS R) . s1
by A1, A6;
then
(
t . x = f . x &
t . y = f . y &
t . x,
t . y are_convertible_wrt (TRS R) . s2 )
by A5, Th47;
hence
[(t . a),(t . b)] in E . s2
by A1;
:: thesis: verum
end;
hence
E is EquationalTheory of A
by A2, A3, MSUALG_4:def 5; :: thesis: verum