set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
defpred S1[ set , set , set ] means for R being monotone OSCongruence of ParsedTermsOSA X holds [$1,$2] in R . $3;
deffunc H1( object ) -> set = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . $1 & y in the Sorts of (ParsedTermsOSA X) . $1 & ( for R being monotone OSCongruence of ParsedTermsOSA X holds [x,y] in R . $1 ) ) } ;
consider f being ManySortedSet of the carrier of S such that
A1:
for i being object st i in the carrier of S holds
f . i = H1(i)
from PBOOLE:sch 4();
A2:
for i being set st i in the carrier of S holds
f . i is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i)
proof
let i be
set ;
( i in the carrier of S implies f . i is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i) )
assume A3:
i in the
carrier of
S
;
f . i is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i)
reconsider s =
i as
Element of
S by A3;
A4:
f . i = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . i & y in the Sorts of (ParsedTermsOSA X) . i & ( for R being monotone OSCongruence of ParsedTermsOSA X holds [x,y] in R . i ) ) }
by A1, A3;
then reconsider fi =
f . i as
Relation of
( the Sorts of (ParsedTermsOSA X) . i) by TARSKI:def 3;
now for x, y, z being object st x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & z in the Sorts of (ParsedTermsOSA X) . s & [x,y] in fi & [y,z] in fi holds
[x,z] in filet x,
y,
z be
object ;
( x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & z in the Sorts of (ParsedTermsOSA X) . s & [x,y] in fi & [y,z] in fi implies [x,z] in fi )assume that A5:
x in the
Sorts of
(ParsedTermsOSA X) . s
and A6:
y in the
Sorts of
(ParsedTermsOSA X) . s
and A7:
z in the
Sorts of
(ParsedTermsOSA X) . s
and A8:
[x,y] in fi
and A9:
[y,z] in fi
;
[x,z] in fithus
[x,z] in fi
verumproof
reconsider t1 =
x,
t2 =
y,
t3 =
z as
Element of
TS (DTConOSA X) by A5, A6, A7, Th15;
A10:
ex
t6,
t7 being
Element of
TS (DTConOSA X) st
(
[t2,t3] = [t6,t7] &
t6 in the
Sorts of
(ParsedTermsOSA X) . i &
t7 in the
Sorts of
(ParsedTermsOSA X) . i &
S1[
t6,
t7,
i] )
by A4, A9;
A11:
ex
t4,
t5 being
Element of
TS (DTConOSA X) st
(
[t1,t2] = [t4,t5] &
t4 in the
Sorts of
(ParsedTermsOSA X) . i &
t5 in the
Sorts of
(ParsedTermsOSA X) . i &
S1[
t4,
t5,
i] )
by A4, A8;
hence
[x,z] in fi
by A4, A5, A7;
verum
end; end;
then A14:
fi is_transitive_in the
Sorts of
(ParsedTermsOSA X) . s
by RELAT_2:def 8;
now for x, y being object st x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & [x,y] in fi holds
[y,x] in filet x,
y be
object ;
( x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & [x,y] in fi implies [y,x] in fi )assume that A15:
x in the
Sorts of
(ParsedTermsOSA X) . s
and A16:
y in the
Sorts of
(ParsedTermsOSA X) . s
and A17:
[x,y] in fi
;
[y,x] in fithus
[y,x] in fi
verumproof
reconsider t1 =
x,
t2 =
y as
Element of
TS (DTConOSA X) by A15, A16, Th15;
A18:
ex
t3,
t4 being
Element of
TS (DTConOSA X) st
(
[t1,t2] = [t3,t4] &
t3 in the
Sorts of
(ParsedTermsOSA X) . i &
t4 in the
Sorts of
(ParsedTermsOSA X) . i &
S1[
t3,
t4,
i] )
by A4, A17;
hence
[y,x] in fi
by A4, A15, A16;
verum
end; end;
then A20:
fi is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . s
by RELAT_2:def 3;
then A22:
fi is_reflexive_in the
Sorts of
(ParsedTermsOSA X) . s
by RELAT_2:def 1;
then A23:
field fi = the
Sorts of
(ParsedTermsOSA X) . s
by ORDERS_1:13;
dom fi = the
Sorts of
(ParsedTermsOSA X) . s
by A22, ORDERS_1:13;
hence
f . i is
Equivalence_Relation of
( the Sorts of (ParsedTermsOSA X) . i)
by A23, A20, A14, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
verum
end;
then
for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of (ParsedTermsOSA X) . i),( the Sorts of (ParsedTermsOSA X) . i)
;
then reconsider f = f as ManySortedRelation of the Sorts of (ParsedTermsOSA X) by MSUALG_4:def 1;
reconsider f = f as ManySortedRelation of (ParsedTermsOSA X) ;
for i being set
for R being Relation of ( the Sorts of (ParsedTermsOSA X) . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i)
by A2;
then
f is MSEquivalence_Relation-like
by MSUALG_4:def 2;
then reconsider f = f as MSEquivalence-like ManySortedRelation of (ParsedTermsOSA X) by MSUALG_4:def 3;
f is os-compatible
proof
let s1,
s2 be
Element of
S;
OSALG_4:def 1 ( not s1 <= s2 or for b1, b2 being set holds
( not b1 in the Sorts of (ParsedTermsOSA X) . s1 or not b2 in the Sorts of (ParsedTermsOSA X) . s1 or ( ( not [b1,b2] in f . s1 or [b1,b2] in f . s2 ) & ( not [b1,b2] in f . s2 or [b1,b2] in f . s1 ) ) ) )
assume A24:
s1 <= s2
;
for b1, b2 being set holds
( not b1 in the Sorts of (ParsedTermsOSA X) . s1 or not b2 in the Sorts of (ParsedTermsOSA X) . s1 or ( ( not [b1,b2] in f . s1 or [b1,b2] in f . s2 ) & ( not [b1,b2] in f . s2 or [b1,b2] in f . s1 ) ) )
A25:
f . s1 = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 & S1[x,y,s1] ) }
by A1;
A26:
f . s2 = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . s2 & y in the Sorts of (ParsedTermsOSA X) . s2 & S1[x,y,s2] ) }
by A1;
let x,
y be
set ;
( not x in the Sorts of (ParsedTermsOSA X) . s1 or not y in the Sorts of (ParsedTermsOSA X) . s1 or ( ( not [x,y] in f . s1 or [x,y] in f . s2 ) & ( not [x,y] in f . s2 or [x,y] in f . s1 ) ) )
assume that A27:
x in the
Sorts of
(ParsedTermsOSA X) . s1
and A28:
y in the
Sorts of
(ParsedTermsOSA X) . s1
;
( ( not [x,y] in f . s1 or [x,y] in f . s2 ) & ( not [x,y] in f . s2 or [x,y] in f . s1 ) )
hereby ( not [x,y] in f . s2 or [x,y] in f . s1 )
end;
assume
[x,y] in f . s2
;
[x,y] in f . s1
then consider t1,
t2 being
Element of
TS (DTConOSA X) such that A34:
[x,y] = [t1,t2]
and
t1 in the
Sorts of
(ParsedTermsOSA X) . s2
and
t2 in the
Sorts of
(ParsedTermsOSA X) . s2
and A35:
S1[
t1,
t2,
s2]
by A26;
A36:
y = t2
by A34, XTUPLE_0:1;
x = t1
by A34, XTUPLE_0:1;
hence
[x,y] in f . s1
by A25, A27, A28, A36, A37;
verum
end;
then reconsider f = f as MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X by OSALG_4:def 2;
f is monotone
proof
let o1,
o2 be
OperSymbol of
S;
OSALG_4:def 26 ( not o1 <= o2 or for b1 being Element of Args (o1,(ParsedTermsOSA X))
for b2 being Element of Args (o2,(ParsedTermsOSA X)) holds
( ex b3 being set st
( b3 in proj1 b1 & not [(b1 . b3),(b2 . b3)] in f . ((the_arity_of o2) /. b3) ) or [((Den (o1,(ParsedTermsOSA X))) . b1),((Den (o2,(ParsedTermsOSA X))) . b2)] in f . (the_result_sort_of o2) ) )
assume A39:
o1 <= o2
;
for b1 being Element of Args (o1,(ParsedTermsOSA X))
for b2 being Element of Args (o2,(ParsedTermsOSA X)) holds
( ex b3 being set st
( b3 in proj1 b1 & not [(b1 . b3),(b2 . b3)] in f . ((the_arity_of o2) /. b3) ) or [((Den (o1,(ParsedTermsOSA X))) . b1),((Den (o2,(ParsedTermsOSA X))) . b2)] in f . (the_result_sort_of o2) )
set w2 =
the_arity_of o2;
set rs2 =
the_result_sort_of o2;
let x1 be
Element of
Args (
o1,
(ParsedTermsOSA X));
for b1 being Element of Args (o2,(ParsedTermsOSA X)) holds
( ex b2 being set st
( b2 in proj1 x1 & not [(x1 . b2),(b1 . b2)] in f . ((the_arity_of o2) /. b2) ) or [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . b1)] in f . (the_result_sort_of o2) )let x2 be
Element of
Args (
o2,
(ParsedTermsOSA X));
( ex b1 being set st
( b1 in proj1 x1 & not [(x1 . b1),(x2 . b1)] in f . ((the_arity_of o2) /. b1) ) or [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in f . (the_result_sort_of o2) )
assume A40:
for
y being
Nat st
y in dom x1 holds
[(x1 . y),(x2 . y)] in f . ((the_arity_of o2) /. y)
;
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in f . (the_result_sort_of o2)
set D1 =
(Den (o1,(ParsedTermsOSA X))) . x1;
set D2 =
(Den (o2,(ParsedTermsOSA X))) . x2;
A41:
now for R being monotone OSCongruence of ParsedTermsOSA X holds
( (Den (o1,(ParsedTermsOSA X))) . x1 in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & (Den (o2,(ParsedTermsOSA X))) . x2 in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . (the_result_sort_of o2) & (Den (o1,(ParsedTermsOSA X))) . x1 is Element of TS (DTConOSA X) & (Den (o2,(ParsedTermsOSA X))) . x2 is Element of TS (DTConOSA X) )let R be
monotone OSCongruence of
ParsedTermsOSA X;
( (Den (o1,(ParsedTermsOSA X))) . x1 in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & (Den (o2,(ParsedTermsOSA X))) . x2 in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . (the_result_sort_of o2) & (Den (o1,(ParsedTermsOSA X))) . x1 is Element of TS (DTConOSA X) & (Den (o2,(ParsedTermsOSA X))) . x2 is Element of TS (DTConOSA X) )A42:
now for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y)let y be
Nat;
( y in dom x1 implies [(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) )assume
y in dom x1
;
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y)then A43:
[(x1 . y),(x2 . y)] in f . ((the_arity_of o2) /. y)
by A40;
f . ((the_arity_of o2) /. y) = { [x,z] where x, z is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o2) /. y) & z in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o2) /. y) & S1[x,z,(the_arity_of o2) /. y] ) }
by A1;
then
ex
x,
z being
Element of
TS (DTConOSA X) st
(
[(x1 . y),(x2 . y)] = [x,z] &
x in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o2) /. y) &
z in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o2) /. y) &
S1[
x,
z,
(the_arity_of o2) /. y] )
by A43;
hence
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y)
;
verum end; then A44:
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . (the_result_sort_of o2)
by A39, OSALG_4:def 26;
then A45:
(Den (o2,(ParsedTermsOSA X))) . x2 in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o2)
by ZFMISC_1:87;
(Den (o1,(ParsedTermsOSA X))) . x1 in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o2)
by A44, ZFMISC_1:87;
hence
(
(Den (o1,(ParsedTermsOSA X))) . x1 in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o2) &
(Den (o2,(ParsedTermsOSA X))) . x2 in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o2) &
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . (the_result_sort_of o2) &
(Den (o1,(ParsedTermsOSA X))) . x1 is
Element of
TS (DTConOSA X) &
(Den (o2,(ParsedTermsOSA X))) . x2 is
Element of
TS (DTConOSA X) )
by A39, A42, A45, Th15, OSALG_4:def 26;
verum end;
f . (the_result_sort_of o2) = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & y in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & S1[x,y, the_result_sort_of o2] ) }
by A1;
hence
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in f . (the_result_sort_of o2)
by A41;
verum
end;
then reconsider f = f as MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X ;
take
f
; for R being monotone OSCongruence of ParsedTermsOSA X holds f c= R
let R be monotone OSCongruence of ParsedTermsOSA X; f c= R
let i be object ; PBOOLE:def 2 ( not i in the carrier of S or f . i c= R . i )
assume
i in the carrier of S
; f . i c= R . i
then reconsider s = i as Element of S ;
A46:
f . s = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & S1[x,y,s] ) }
by A1;
let z be object ; TARSKI:def 3 ( not z in f . i or z in R . i )
assume
z in f . i
; z in R . i
then
ex x, y being Element of TS (DTConOSA X) st
( z = [x,y] & x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & S1[x,y,s] )
by A46;
hence
z in R . i
; verum