let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V5 ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R
let X be V5 ManySortedSet of S; :: thesis: 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; :: thesis: PTCongruence X c= R
A1:
R is os-compatible
by OSALG_4:def 3;
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or (PTCongruence X) . i c= R . i )
assume A2:
i in the carrier of S
; :: thesis: (PTCongruence X) . i c= R . i
reconsider s = i as Element of S by A2;
for a, b being set st [a,b] in (PTCongruence X) . s holds
[a,b] in R . s
proof
let a,
b be
set ;
:: thesis: ( [a,b] in (PTCongruence X) . s implies [a,b] in R . s )
assume A3:
[a,b] in (PTCongruence X) . s
;
:: thesis: [a,b] in R . s
A4:
(
a in the
Sorts of
(ParsedTermsOSA X) . i &
b in the
Sorts of
(ParsedTermsOSA X) . i )
by A3, ZFMISC_1:106;
reconsider ta =
a,
tb =
b as
Element of the
Sorts of
(ParsedTermsOSA X) . s by A3, ZFMISC_1:106;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PBOOLE:def 3;
then reconsider t1 =
a,
t2 =
b as
Element of
(ParsedTermsOSA X) by A2, A4, CARD_5:10;
reconsider t1 =
t1,
t2 =
t2 as
Element of
TS (DTConOSA X) by Th15;
A5:
(
t1 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t1) &
t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2) &
(PTMin X) . t1 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort ((PTMin X) . t1)) &
(PTMin X) . t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort ((PTMin X) . t2)) &
LeastSort t1 <= s &
LeastSort t2 <= s )
by A4, Def12;
A6:
OSClass (PTCongruence X),
ta = OSClass (PTCongruence X),
tb
by A3, OSALG_4:13;
(
OSClass (PTCongruence X),
t1 = OSClass (PTCongruence X),
ta &
OSClass (PTCongruence X),
t2 = OSClass (PTCongruence X),
tb )
by Def28;
then
t1 in OSClass (PTCongruence X),
t2
by A6, Th35;
then A7:
(PTMin X) . t1 = (PTMin X) . t2
by Th43;
(
LeastSort ((PTMin X) . t1) <= LeastSort t1 &
LeastSort ((PTMin X) . t2) <= LeastSort t2 )
by Th41;
then A8:
(
O1 . (LeastSort ((PTMin X) . t1)) c= O1 . (LeastSort t1) &
O1 . (LeastSort ((PTMin X) . t2)) c= O1 . (LeastSort t2) )
by OSALG_1:def 18;
(
[t1,((PTMin X) . t1)] in R . (LeastSort t1) &
[t2,((PTMin X) . t2)] in R . (LeastSort t2) )
by Th45;
then A9:
(
[t1,((PTMin X) . t1)] in R . s &
[t2,((PTMin X) . t2)] in R . s )
by A1, A5, A8, OSALG_4:def 1;
then A10:
(
(PTMin X) . t1 in the
Sorts of
(ParsedTermsOSA X) . s &
(PTMin X) . t2 in the
Sorts of
(ParsedTermsOSA X) . s )
by ZFMISC_1:106;
field (R . s) = the
Sorts of
(ParsedTermsOSA X) . s
by ORDERS_1:97;
then A11:
(
R . s is_transitive_in the
Sorts of
(ParsedTermsOSA X) . s &
R . s is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . s )
by RELAT_2:def 11, RELAT_2:def 16;
then
[((PTMin X) . t2),t2] in R . s
by A4, A9, A10, RELAT_2:def 3;
hence
[a,b] in R . s
by A4, A7, A9, A10, A11, RELAT_2:def 8;
:: thesis: verum
end;
hence
(PTCongruence X) . i c= R . i
by RELAT_1:def 3; :: thesis: verum