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
A5:
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 A5, Th50;
take
P
; ( R c= P & ( for Q being EquationalTheory of A st R c= Q holds
P c= Q ) )
thus
R c= P
for Q being EquationalTheory of A st R c= Q holds
P c= Qproof
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 A6:
[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 A6, REWRITE1:29;
hence
[x,y] in P . s
by A5;
verum
end;
hence
R . i c= P . i
;
verum
end;
let Q be EquationalTheory of A; ( R c= Q implies P c= Q )
assume A7:
R c= Q
; P c= Q
let i be object ; PBOOLE:def 2 ( not i in the carrier of S or P . i c= Q . i )
assume
i in the carrier of S
; P . i c= Q . i
then reconsider s = i as SortSymbol of S ;
A8:
TRS R c= Q
by A7, Def13;
P . s c= Q . s
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in P . s or [x,y] in Q . s )
assume A9:
[x,y] in P . s
;
[x,y] in Q . s
then reconsider a =
x,
b =
y as
Element of
A,
s by ZFMISC_1:87;
a,
b are_convertible_wrt (TRS R) . s
by A5, A9;
hence
[x,y] in Q . s
by A8, Th51;
verum
end;
hence
P . i c= Q . i
; verum