let S be monotone regular locally_directed OrderSortedSign; for X being non-empty ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R
let X be non-empty ManySortedSet of S; for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set M = PTMin X;
set P = PTCongruence X;
reconsider O1 = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of S ;
let R be MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X; PTCongruence X c= R
let i be object ; PBOOLE:def 2 ( not i in the carrier of S or (PTCongruence X) . i c= R . i )
assume A1:
i in the carrier of S
; (PTCongruence X) . i c= R . i
reconsider s = i as Element of S by A1;
A2:
R is os-compatible
by OSALG_4:def 2;
for a, b being object st [a,b] in (PTCongruence X) . s holds
[a,b] in R . s
proof
A3:
field (R . s) = the
Sorts of
(ParsedTermsOSA X) . s
by ORDERS_1:12;
then A4:
R . s is_transitive_in the
Sorts of
(ParsedTermsOSA X) . s
by RELAT_2:def 16;
A5:
R . s is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . s
by A3, RELAT_2:def 11;
let a,
b be
object ;
( [a,b] in (PTCongruence X) . s implies [a,b] in R . s )
assume A6:
[a,b] in (PTCongruence X) . s
;
[a,b] in R . s
reconsider ta =
a,
tb =
b as
Element of the
Sorts of
(ParsedTermsOSA X) . s by A6, ZFMISC_1:87;
A7:
a in the
Sorts of
(ParsedTermsOSA X) . i
by A6, ZFMISC_1:87;
A8:
OSClass (
(PTCongruence X),
ta)
= OSClass (
(PTCongruence X),
tb)
by A6, OSALG_4:12;
A9:
b in the
Sorts of
(ParsedTermsOSA X) . i
by A6, ZFMISC_1:87;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 2;
then reconsider t1 =
a,
t2 =
b as
Element of
(ParsedTermsOSA X) by A1, A7, A9, CARD_5:2;
reconsider t1 =
t1,
t2 =
t2 as
Element of
TS (DTConOSA X) by Th14;
A10:
t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2)
by Def12;
A11:
(PTMin X) . t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort ((PTMin X) . t2))
by Def12;
LeastSort ((PTMin X) . t2) <= LeastSort t2
by Th40;
then A12:
O1 . (LeastSort ((PTMin X) . t2)) c= O1 . (LeastSort t2)
by OSALG_1:def 16;
A13:
[t2,((PTMin X) . t2)] in R . (LeastSort t2)
by Th44;
LeastSort t2 <= s
by A9, Def12;
then A14:
[t2,((PTMin X) . t2)] in R . s
by A2, A10, A11, A12, A13;
then
(PTMin X) . t2 in the
Sorts of
(ParsedTermsOSA X) . s
by ZFMISC_1:87;
then A15:
[((PTMin X) . t2),t2] in R . s
by A9, A14, A5, RELAT_2:def 3;
LeastSort ((PTMin X) . t1) <= LeastSort t1
by Th40;
then A16:
O1 . (LeastSort ((PTMin X) . t1)) c= O1 . (LeastSort t1)
by OSALG_1:def 16;
A17:
(PTMin X) . t1 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort ((PTMin X) . t1))
by Def12;
A18:
[t1,((PTMin X) . t1)] in R . (LeastSort t1)
by Th44;
A19:
OSClass (
(PTCongruence X),
t2)
= OSClass (
(PTCongruence X),
tb)
by Def27;
OSClass (
(PTCongruence X),
t1)
= OSClass (
(PTCongruence X),
ta)
by Def27;
then
t1 in OSClass (
(PTCongruence X),
t2)
by A8, A19, Th34;
then A20:
(PTMin X) . t1 = (PTMin X) . t2
by Th42;
A21:
t1 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t1)
by Def12;
LeastSort t1 <= s
by A7, Def12;
then A22:
[t1,((PTMin X) . t1)] in R . s
by A2, A21, A17, A16, A18;
then
(PTMin X) . t1 in the
Sorts of
(ParsedTermsOSA X) . s
by ZFMISC_1:87;
hence
[a,b] in R . s
by A7, A9, A20, A22, A4, A15, RELAT_2:def 8;
verum
end;
hence
(PTCongruence X) . i c= R . i
by RELAT_1:def 3; verum