let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for x, y, z being Element of TS (DTConOSA X)
for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds
[x,s] in (PTClasses X) . z
let X be V2() ManySortedSet of S; for x, y, z being Element of TS (DTConOSA X)
for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds
[x,s] in (PTClasses X) . z
set D = DTConOSA X;
set PTA = ParsedTermsOSA X;
set C = bool [:(TS (DTConOSA X)), the carrier of S:];
set SPTA = the Sorts of (ParsedTermsOSA X);
set F = PTClasses X;
defpred S1[ set ] means for s being Element of S
for y, z being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . $1 & [z,s] in (PTClasses X) . y holds
[$1,s] in (PTClasses X) . z;
A1:
for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let nt be
Symbol of
(DTConOSA X);
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS (DTConOSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that A2:
nt ==> roots ts
and A3:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S1[
t]
;
S1[nt -tree ts]
consider o being
OperSymbol of
S such that A4:
nt = [o, the carrier of S]
and A5:
ts in Args (
o,
(ParsedTermsOSA X))
and A6:
nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts
and
for
s1 being
Element of
S holds
(
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s1 iff
the_result_sort_of o <= s1 )
by A2, Th12;
reconsider ts1 =
ts as
Element of
Args (
o,
(ParsedTermsOSA X))
by A5;
set w =
the_arity_of o;
A7:
dom (the_arity_of o) = dom ts
by A5, MSUALG_3:6;
reconsider x =
(PTClasses X) * ts as
FinSequence of
bool [:(TS (DTConOSA X)), the carrier of S:] ;
A8:
rng ts c= TS (DTConOSA X)
by FINSEQ_1:def 4;
dom (PTClasses X) = TS (DTConOSA X)
by FUNCT_2:def 1;
then
len x = len ts
by A8, FINSEQ_2:29;
then A9:
dom x = dom ts
by FINSEQ_3:29;
A10:
(PTClasses X) . (nt -tree ts) =
@ (
nt,
x)
by A2, Def21
.=
{ [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) }
;
thus
S1[
nt -tree ts]
verumproof
let s1 be
Element of
S;
for y, z being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (nt -tree ts) & [z,s1] in (PTClasses X) . y holds
[(nt -tree ts),s1] in (PTClasses X) . zlet y,
z be
Element of
TS (DTConOSA X);
( [y,s1] in (PTClasses X) . (nt -tree ts) & [z,s1] in (PTClasses X) . y implies [(nt -tree ts),s1] in (PTClasses X) . z )
assume that A11:
[y,s1] in (PTClasses X) . (nt -tree ts)
and A12:
[z,s1] in (PTClasses X) . y
;
[(nt -tree ts),s1] in (PTClasses X) . z
consider o2 being
OperSymbol of
S,
x2 being
Element of
Args (
o2,
(ParsedTermsOSA X)),
s3 being
Element of
S such that A13:
[y,s1] = [((Den (o2,(ParsedTermsOSA X))) . x2),s3]
and A14:
ex
o1 being
OperSymbol of
S st
(
nt = [o1, the carrier of S] &
o1 ~= o2 &
len (the_arity_of o1) = len (the_arity_of o2) &
the_result_sort_of o1 <= s3 &
the_result_sort_of o2 <= s3 )
and A15:
ex
w3 being
Element of the
carrier of
S * st
(
dom w3 = dom x & ( for
y being
Nat st
y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) )
by A10, A11;
A16:
y = (Den (o2,(ParsedTermsOSA X))) . x2
by A13, XTUPLE_0:1;
reconsider x3 =
x2 as
FinSequence of
TS (DTConOSA X) by Th13;
reconsider xy =
(PTClasses X) * x3 as
FinSequence of
bool [:(TS (DTConOSA X)), the carrier of S:] ;
A17:
OSSym (
o2,
X)
==> roots x2
by Th13;
then consider o3 being
OperSymbol of
S such that A18:
OSSym (
o2,
X)
= [o3, the carrier of S]
and
x3 in Args (
o3,
(ParsedTermsOSA X))
and A19:
(OSSym (o2,X)) -tree x3 = (Den (o3,(ParsedTermsOSA X))) . x3
and
for
s2 being
Element of
S holds
(
(OSSym (o2,X)) -tree x3 in the
Sorts of
(ParsedTermsOSA X) . s2 iff
the_result_sort_of o3 <= s2 )
by Th12;
o2 = o3
by A18, XTUPLE_0:1;
then (PTClasses X) . y =
@ (
(OSSym (o2,X)),
xy)
by A16, A17, A19, Def21
.=
{ [((Den (o4,(ParsedTermsOSA X))) . x4),s4] where o4 is OperSymbol of S, x4 is Element of Args (o4,(ParsedTermsOSA X)), s4 is Element of S : ( ex o1 being OperSymbol of S st
( OSSym (o2,X) = [o1, the carrier of S] & o1 ~= o4 & len (the_arity_of o1) = len (the_arity_of o4) & the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) & ex w4 being Element of the carrier of S * st
( dom w4 = dom xy & ( for y being Nat st y in dom xy holds
[(x4 . y),(w4 /. y)] in xy . y ) ) ) }
;
then consider o5 being
OperSymbol of
S,
x5 being
Element of
Args (
o5,
(ParsedTermsOSA X)),
s5 being
Element of
S such that A20:
[z,s1] = [((Den (o5,(ParsedTermsOSA X))) . x5),s5]
and A21:
ex
o1 being
OperSymbol of
S st
(
OSSym (
o2,
X)
= [o1, the carrier of S] &
o1 ~= o5 &
len (the_arity_of o1) = len (the_arity_of o5) &
the_result_sort_of o1 <= s5 &
the_result_sort_of o5 <= s5 )
and A22:
ex
w3 being
Element of the
carrier of
S * st
(
dom w3 = dom xy & ( for
y being
Nat st
y in dom xy holds
[(x5 . y),(w3 /. y)] in xy . y ) )
by A12;
consider o6 being
OperSymbol of
S such that A23:
OSSym (
o2,
X)
= [o6, the carrier of S]
and A24:
o6 ~= o5
and A25:
len (the_arity_of o6) = len (the_arity_of o5)
and
the_result_sort_of o6 <= s5
and A26:
the_result_sort_of o5 <= s5
by A21;
A27:
the_result_sort_of o5 <= s1
by A20, A26, XTUPLE_0:1;
reconsider x6 =
x5 as
FinSequence of
TS (DTConOSA X) by Th13;
reconsider xz =
(PTClasses X) * x6 as
FinSequence of
bool [:(TS (DTConOSA X)), the carrier of S:] ;
defpred S2[
object ,
object ]
means [(ts1 . $1),$2] in xz . $1;
rng x3 c= TS (DTConOSA X)
by FINSEQ_1:def 4;
then
rng x3 c= dom (PTClasses X)
by FUNCT_2:def 1;
then
len xy = len x3
by FINSEQ_2:29;
then A28:
dom x3 = dom xy
by FINSEQ_3:29;
consider w5 being
Element of the
carrier of
S * such that
dom w5 = dom xy
and A29:
for
y being
Nat st
y in dom xy holds
[(x5 . y),(w5 /. y)] in xy . y
by A22;
consider w3 being
Element of the
carrier of
S * such that
dom w3 = dom x
and A30:
for
y being
Nat st
y in dom x holds
[(x2 . y),(w3 /. y)] in x . y
by A15;
A31:
z = (Den (o5,(ParsedTermsOSA X))) . x5
by A20, XTUPLE_0:1;
A32:
OSSym (
o5,
X)
==> roots x5
by Th13;
then consider o7 being
OperSymbol of
S such that A33:
OSSym (
o5,
X)
= [o7, the carrier of S]
and
x6 in Args (
o7,
(ParsedTermsOSA X))
and A34:
(OSSym (o5,X)) -tree x6 = (Den (o7,(ParsedTermsOSA X))) . x6
and
for
s2 being
Element of
S holds
(
(OSSym (o5,X)) -tree x6 in the
Sorts of
(ParsedTermsOSA X) . s2 iff
the_result_sort_of o7 <= s2 )
by Th12;
o5 = o7
by A33, XTUPLE_0:1;
then A35:
(PTClasses X) . z =
@ (
(OSSym (o5,X)),
xz)
by A31, A32, A34, Def21
.=
{ [((Den (o4,(ParsedTermsOSA X))) . x4),s4] where o4 is OperSymbol of S, x4 is Element of Args (o4,(ParsedTermsOSA X)), s4 is Element of S : ( ex o1 being OperSymbol of S st
( OSSym (o5,X) = [o1, the carrier of S] & o1 ~= o4 & len (the_arity_of o1) = len (the_arity_of o4) & the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) & ex w4 being Element of the carrier of S * st
( dom w4 = dom xz & ( for y being Nat st y in dom xz holds
[(x4 . y),(w4 /. y)] in xz . y ) ) ) }
;
consider o1 being
OperSymbol of
S such that A36:
nt = [o1, the carrier of S]
and A37:
o1 ~= o2
and A38:
len (the_arity_of o1) = len (the_arity_of o2)
and A39:
the_result_sort_of o1 <= s3
and
the_result_sort_of o2 <= s3
by A14;
A40:
o1 = o
by A4, A36, XTUPLE_0:1;
then A41:
the_result_sort_of o <= s1
by A13, A39, XTUPLE_0:1;
A42:
dom (the_arity_of o2) = dom (the_arity_of o)
by A38, A40, FINSEQ_3:29;
then A43:
dom x2 = dom x
by A9, A7, MSUALG_3:6;
A44:
rng x6 c= TS (DTConOSA X)
by FINSEQ_1:def 4;
then
rng x6 c= dom (PTClasses X)
by FUNCT_2:def 1;
then
len xz = len x6
by FINSEQ_2:29;
then A45:
dom x6 = dom xz
by FINSEQ_3:29;
A46:
o6 = o2
by A23, XTUPLE_0:1;
then
dom (the_arity_of o5) = dom (the_arity_of o2)
by A25, FINSEQ_3:29;
then A47:
dom x5 =
dom (the_arity_of o2)
by MSUALG_3:6
.=
dom xy
by A28, MSUALG_3:6
;
A48:
rng x3 c= TS (DTConOSA X)
by FINSEQ_1:def 4;
A49:
for
y being
object st
y in dom xz holds
ex
sy being
object st
(
sy in the
carrier of
S &
S2[
y,
sy] )
proof
let y be
object ;
( y in dom xz implies ex sy being object st
( sy in the carrier of S & S2[y,sy] ) )
assume A50:
y in dom xz
;
ex sy being object st
( sy in the carrier of S & S2[y,sy] )
A51:
x5 . y in rng x6
by A45, A50, FUNCT_1:3;
A52:
x2 . y in rng x3
by A28, A45, A47, A50, FUNCT_1:3;
ts1 . y in rng ts1
by A9, A28, A43, A45, A47, A50, FUNCT_1:3;
then reconsider t1 =
ts1 . y,
t2 =
x3 . y,
t3 =
x5 . y as
Element of
TS (DTConOSA X) by A8, A44, A48, A51, A52;
A53:
[(x2 . y),(w3 /. y)] in x . y
by A30, A28, A43, A45, A47, A50;
y in dom ts1
by A7, A42, A28, A45, A47, A50, MSUALG_3:6;
then A54:
[t2,(w3 /. y)] in (PTClasses X) . t1
by A53, FUNCT_1:13;
then
[t1,(w3 /. y)] in (PTClasses X) . t1
by Th20;
then A55:
t1 in the
Sorts of
(ParsedTermsOSA X) . (w3 /. y)
by Th19;
[t1,(w3 /. y)] in (PTClasses X) . t2
by A54, Th19;
then
[t2,(w3 /. y)] in (PTClasses X) . t2
by Th20;
then A56:
t2 in the
Sorts of
(ParsedTermsOSA X) . (w3 /. y)
by Th19;
then A57:
LeastSort t2 <= w3 /. y
by Def12;
[(x5 . y),(w5 /. y)] in xy . y
by A29, A45, A47, A50;
then A58:
[t3,(w5 /. y)] in (PTClasses X) . t2
by A28, A45, A47, A50, FUNCT_1:13;
then
[t2,(w5 /. y)] in (PTClasses X) . t2
by Th20;
then A59:
t2 in the
Sorts of
(ParsedTermsOSA X) . (w5 /. y)
by Th19;
then
LeastSort t2 <= w5 /. y
by Def12;
then consider s7 being
Element of
S such that A60:
w5 /. y <= s7
and A61:
w3 /. y <= s7
by A57, OSALG_4:11;
[t2,(w5 /. y)] in (PTClasses X) . t3
by A58, Th19;
then
[t3,(w5 /. y)] in (PTClasses X) . t3
by Th20;
then
t3 in the
Sorts of
(ParsedTermsOSA X) . (w5 /. y)
by Th19;
then A62:
[t3,s7] in (PTClasses X) . t2
by A58, A59, A60, Th21;
take
s7
;
( s7 in the carrier of S & S2[y,s7] )
thus
s7 in the
carrier of
S
;
S2[y,s7]
[(x2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y)
by A9, A28, A43, A45, A47, A50, A53, FUNCT_1:13;
then
[t2,s7] in (PTClasses X) . t1
by A56, A55, A61, Th21;
then
[t1,s7] in (PTClasses X) . t3
by A3, A9, A28, A43, A45, A47, A50, A62, FUNCT_1:3;
hence
S2[
y,
s7]
by A50, FUNCT_1:12;
verum
end;
consider f being
Function of
(dom xz), the
carrier of
S such that A63:
for
y being
object st
y in dom xz holds
S2[
y,
f . y]
from FUNCT_2:sch 1(A49);
A64:
dom f = dom xz
by FUNCT_2:def 1;
then
ex
n being
Nat st
dom f = Seg n
by FINSEQ_1:def 2;
then reconsider f1 =
f as
FinSequence by FINSEQ_1:def 2;
rng f c= the
carrier of
S
by RELAT_1:def 19;
then
f1 is
FinSequence of the
carrier of
S
by FINSEQ_1:def 4;
then reconsider f =
f as
Element of the
carrier of
S * by FINSEQ_1:def 11;
A65:
(
dom f = dom xz & ( for
y being
Nat st
y in dom xz holds
[(ts1 . y),(f /. y)] in xz . y ) )
o5 ~= o
by A37, A40, A24, A46, OSALG_1:2;
hence
[(nt -tree ts),s1] in (PTClasses X) . z
by A6, A38, A40, A25, A46, A65, A35, A27, A41;
verum
end;
end;
A67:
for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S1[ root-tree s]
proof
let sy be
Symbol of
(DTConOSA X);
( sy in Terminals (DTConOSA X) implies S1[ root-tree sy] )
assume
sy in Terminals (DTConOSA X)
;
S1[ root-tree sy]
then A68:
(PTClasses X) . (root-tree sy) =
@ sy
by Def21
.=
{ [(root-tree sy),s1] where s1 is Element of S : ex s2 being Element of S ex x being set st
( x in X . s2 & sy = [x,s2] & s2 <= s1 ) }
;
thus
S1[
root-tree sy]
verumproof
let s1 be
Element of
S;
for y, z being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (root-tree sy) & [z,s1] in (PTClasses X) . y holds
[(root-tree sy),s1] in (PTClasses X) . zlet y,
z be
Element of
TS (DTConOSA X);
( [y,s1] in (PTClasses X) . (root-tree sy) & [z,s1] in (PTClasses X) . y implies [(root-tree sy),s1] in (PTClasses X) . z )
assume that A69:
[y,s1] in (PTClasses X) . (root-tree sy)
and A70:
[z,s1] in (PTClasses X) . y
;
[(root-tree sy),s1] in (PTClasses X) . z
ex
s2 being
Element of
S st
(
[y,s1] = [(root-tree sy),s2] & ex
s0 being
Element of
S ex
x being
set st
(
x in X . s0 &
sy = [x,s0] &
s0 <= s2 ) )
by A68, A69;
then A71:
y = root-tree sy
by XTUPLE_0:1;
then
ex
s3 being
Element of
S st
(
[z,s1] = [(root-tree sy),s3] & ex
s0 being
Element of
S ex
x being
set st
(
x in X . s0 &
sy = [x,s0] &
s0 <= s3 ) )
by A68, A70;
hence
[(root-tree sy),s1] in (PTClasses X) . z
by A69, A71, XTUPLE_0:1;
verum
end;
end;
for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S1[t]
from DTCONSTR:sch 7(A67, A1);
hence
for x, y, z being Element of TS (DTConOSA X)
for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds
[x,s] in (PTClasses X) . z
; verum