let S be 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 )
let A be 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 )
let R be 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 )
let s be 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 )
let a, b be Element of A,s; ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s )
defpred S1[ SortSymbol of S, set , set ] means $2,$3 are_convertible_wrt (TRS R) . $1;
consider P being ManySortedRelation of the Sorts of A such that
A1:
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in P . s iff S1[s,a,b] )
from MSUALG_6:sch 2();
reconsider P = P as ManySortedRelation of A ;
reconsider P = P as EquationalTheory of A by A1, Th50;
R c= P
proof
let i be
object ;
PBOOLE:def 2 ( not i in the carrier of S or R . i c= P . i )
assume
i in the
carrier of
S
;
R . i c= P . i
then reconsider s =
i as
SortSymbol of
S ;
R . s c= P . s
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in R . s or [x,y] in P . s )
assume A2:
[x,y] in R . s
;
[x,y] in P . s
then reconsider a =
x,
b =
y as
Element of
A,
s by ZFMISC_1:87;
R c= TRS R
by Def13;
then
R . s c= (TRS R) . s
;
then
a,
b are_convertible_wrt (TRS R) . s
by A2, REWRITE1:29;
hence
[x,y] in P . s
by A1;
verum
end;
hence
R . i c= P . i
;
verum
end;
then
EqTh R c= P
by Def15;
then
(EqTh R) . s c= P . s
;
hence
( [a,b] in (EqTh R) . s implies a,b are_convertible_wrt (TRS R) . s )
by A1; ( a,b are_convertible_wrt (TRS R) . s implies [a,b] in (EqTh R) . s )
R c= EqTh R
by Def15;
then
TRS R c= EqTh R
by Def13;
hence
( a,b are_convertible_wrt (TRS R) . s implies [a,b] in (EqTh R) . s )
by Th51; verum