set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set F = PTClasses X;
deffunc H1( object ) -> set = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,$1] in (PTClasses X) . y } ;
consider R being ManySortedSet of the carrier of S such that
A1:
for i being object st i in the carrier of S holds
R . i = H1(i)
from PBOOLE:sch 4();
for i being set st i in the carrier of S holds
R . i is Relation of ( the Sorts of (ParsedTermsOSA X) . i)
proof
let i be
set ;
( i in the carrier of S implies R . i is Relation of ( the Sorts of (ParsedTermsOSA X) . i) )
assume A2:
i in the
carrier of
S
;
R . i is Relation of ( the Sorts of (ParsedTermsOSA X) . i)
reconsider s =
i as
Element of
S by A2;
A3:
R . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y }
by A1, A2;
R . s c= [:( the Sorts of (ParsedTermsOSA X) . s),( the Sorts of (ParsedTermsOSA X) . s):]
proof
let z be
object ;
TARSKI:def 3 ( not z in R . s or z in [:( the Sorts of (ParsedTermsOSA X) . s),( the Sorts of (ParsedTermsOSA X) . s):] )
assume
z in R . s
;
z in [:( the Sorts of (ParsedTermsOSA X) . s),( the Sorts of (ParsedTermsOSA X) . s):]
then consider x,
y being
Element of
TS (DTConOSA X) such that A4:
z = [x,y]
and A5:
[x,s] in (PTClasses X) . y
by A3;
[y,s] in (PTClasses X) . x
by A5, Th19;
then
[x,s] in (PTClasses X) . x
by Th20;
then A6:
x in the
Sorts of
(ParsedTermsOSA X) . s
by Th19;
[y,s] in (PTClasses X) . y
by A5, Th20;
then
y in the
Sorts of
(ParsedTermsOSA X) . s
by Th19;
hence
z in [:( the Sorts of (ParsedTermsOSA X) . s),( the Sorts of (ParsedTermsOSA X) . s):]
by A4, A6, ZFMISC_1:87;
verum
end;
hence
R . i is
Relation of
( the Sorts of (ParsedTermsOSA X) . i)
;
verum
end;
then reconsider R = R as ManySortedRelation of (ParsedTermsOSA X) by MSUALG_4:def 1;
for s1, s2 being Element of S st s1 <= s2 holds
for x, y being set st x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [x,y] in R . s1 iff [x,y] in R . s2 )
proof
let s1,
s2 be
Element of
S;
( s1 <= s2 implies for x, y being set st x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [x,y] in R . s1 iff [x,y] in R . s2 ) )
assume A7:
s1 <= s2
;
for x, y being set st x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [x,y] in R . s1 iff [x,y] in R . s2 )
A8:
R . s1 = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,s1] in (PTClasses X) . y }
by A1;
A9:
R . s2 = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,s2] in (PTClasses X) . y }
by A1;
let x,
y be
set ;
( x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 implies ( [x,y] in R . s1 iff [x,y] in R . s2 ) )
assume that A10:
x in the
Sorts of
(ParsedTermsOSA X) . s1
and A11:
y in the
Sorts of
(ParsedTermsOSA X) . s1
;
( [x,y] in R . s1 iff [x,y] in R . s2 )
hereby ( [x,y] in R . s2 implies [x,y] in R . s1 )
assume
[x,y] in R . s1
;
[x,y] in R . s2then consider t1,
t2 being
Element of
TS (DTConOSA X) such that A12:
[x,y] = [t1,t2]
and A13:
[t1,s1] in (PTClasses X) . t2
by A8;
A14:
y = t2
by A12, XTUPLE_0:1;
x = t1
by A12, XTUPLE_0:1;
then
[t1,s2] in (PTClasses X) . t2
by A7, A10, A11, A13, A14, Th21;
hence
[x,y] in R . s2
by A9, A12;
verum
end;
assume
[x,y] in R . s2
;
[x,y] in R . s1
then consider t1,
t2 being
Element of
TS (DTConOSA X) such that A15:
[x,y] = [t1,t2]
and A16:
[t1,s2] in (PTClasses X) . t2
by A9;
A17:
y = t2
by A15, XTUPLE_0:1;
x = t1
by A15, XTUPLE_0:1;
then
[t1,s1] in (PTClasses X) . t2
by A7, A10, A11, A16, A17, Th21;
hence
[x,y] in R . s1
by A8, A15;
verum
end;
then A18:
R is os-compatible
;
defpred S1[ Element of TS (DTConOSA X), Element of S] means ( ex s1 being Element of S ex x being object st
( s1 <= $2 & x in X . s1 & $1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = $1 . {} & the_result_sort_of o <= $2 ) );
reconsider R = R as OrderSortedRelation of ParsedTermsOSA X by A18, OSALG_4:def 2;
for i being set
for Ri being Relation of ( the Sorts of (ParsedTermsOSA X) . i) st i in the carrier of S & R . i = Ri holds
Ri is total symmetric transitive Relation of ( the Sorts of (ParsedTermsOSA X) . i)
proof
let i be
set ;
for Ri being Relation of ( the Sorts of (ParsedTermsOSA X) . i) st i in the carrier of S & R . i = Ri holds
Ri is total symmetric transitive Relation of ( the Sorts of (ParsedTermsOSA X) . i)let Ri be
Relation of
( the Sorts of (ParsedTermsOSA X) . i);
( i in the carrier of S & R . i = Ri implies Ri is total symmetric transitive Relation of ( the Sorts of (ParsedTermsOSA X) . i) )
assume that A19:
i in the
carrier of
S
and A20:
R . i = Ri
;
Ri is total symmetric transitive Relation of ( the Sorts of (ParsedTermsOSA X) . i)
reconsider s =
i as
Element of
S by A19;
A21:
Ri = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y }
by A1, A19, A20;
for
x,
y being
object st
x in the
Sorts of
(ParsedTermsOSA X) . i &
y in the
Sorts of
(ParsedTermsOSA X) . i &
[x,y] in Ri holds
[y,x] in Ri
proof
let x,
y be
object ;
( x in the Sorts of (ParsedTermsOSA X) . i & y in the Sorts of (ParsedTermsOSA X) . i & [x,y] in Ri implies [y,x] in Ri )
assume that
x in the
Sorts of
(ParsedTermsOSA X) . i
and
y in the
Sorts of
(ParsedTermsOSA X) . i
and A22:
[x,y] in Ri
;
[y,x] in Ri
consider t1,
t2 being
Element of
TS (DTConOSA X) such that A23:
[x,y] = [t1,t2]
and A24:
[t1,s] in (PTClasses X) . t2
by A21, A22;
A25:
x = t1
by A23, XTUPLE_0:1;
A26:
y = t2
by A23, XTUPLE_0:1;
[t2,s] in (PTClasses X) . t1
by A24, Th19;
hence
[y,x] in Ri
by A21, A25, A26;
verum
end;
then A27:
Ri is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . i
by RELAT_2:def 3;
now for x, y, z being object st x in the Sorts of (ParsedTermsOSA X) . i & y in the Sorts of (ParsedTermsOSA X) . i & z in the Sorts of (ParsedTermsOSA X) . i & [x,y] in Ri & [y,z] in Ri holds
[x,z] in Rilet x,
y,
z be
object ;
( x in the Sorts of (ParsedTermsOSA X) . i & y in the Sorts of (ParsedTermsOSA X) . i & z in the Sorts of (ParsedTermsOSA X) . i & [x,y] in Ri & [y,z] in Ri implies [x,z] in Ri )assume that
x in the
Sorts of
(ParsedTermsOSA X) . i
and
y in the
Sorts of
(ParsedTermsOSA X) . i
and
z in the
Sorts of
(ParsedTermsOSA X) . i
and A28:
[x,y] in Ri
and A29:
[y,z] in Ri
;
[x,z] in Riconsider t1,
t2 being
Element of
TS (DTConOSA X) such that A30:
[x,y] = [t1,t2]
and A31:
[t1,s] in (PTClasses X) . t2
by A21, A28;
A32:
[t2,s] in (PTClasses X) . t1
by A31, Th19;
consider t22,
t3 being
Element of
TS (DTConOSA X) such that A33:
[y,z] = [t22,t3]
and A34:
[t22,s] in (PTClasses X) . t3
by A21, A29;
A35:
y = t22
by A33, XTUPLE_0:1;
y = t2
by A30, XTUPLE_0:1;
then
[t3,s] in (PTClasses X) . t2
by A34, A35, Th19;
then A36:
[t1,s] in (PTClasses X) . t3
by A32, Th22;
A37:
z = t3
by A33, XTUPLE_0:1;
x = t1
by A30, XTUPLE_0:1;
hence
[x,z] in Ri
by A21, A37, A36;
verum end;
then A38:
Ri is_transitive_in the
Sorts of
(ParsedTermsOSA X) . i
by RELAT_2:def 8;
A39:
the
Sorts of
(ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : S1[a,s] }
by Th9;
then A42:
Ri is_reflexive_in the
Sorts of
(ParsedTermsOSA X) . i
by RELAT_2:def 1;
then A43:
field Ri = the
Sorts of
(ParsedTermsOSA X) . i
by ORDERS_1:13;
dom Ri = the
Sorts of
(ParsedTermsOSA X) . i
by A42, ORDERS_1:13;
hence
Ri is
total symmetric transitive Relation of
( the Sorts of (ParsedTermsOSA X) . i)
by A43, A27, A38, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
verum
end;
then
R is MSEquivalence_Relation-like
by MSUALG_4:def 2;
then reconsider R = R as MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X by MSUALG_4:def 3;
take
R
; for i being set st i in the carrier of S holds
R . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y }
thus
for i being set st i in the carrier of S holds
R . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y }
by A1; verum