let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for t being Element of TS (DTConOSA X) holds
( ( for s being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S
for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . y ) )
let X be V2() ManySortedSet of S; for t being Element of TS (DTConOSA X) holds
( ( for s being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S
for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . y ) )
let t be Element of TS (DTConOSA X); ( ( for s being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S
for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . y ) )
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set C = bool [:(TS (DTConOSA X)), the carrier of S:];
set F = PTClasses X;
defpred S1[ set ] means for s being Element of S holds
( $1 in the Sorts of (ParsedTermsOSA X) . s iff [$1,s] in (PTClasses X) . $1 );
defpred S2[ set ] means for s being Element of S
for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . $1 holds
[$1,s] in (PTClasses X) . y;
defpred S3[ DecoratedTree of the carrier of (DTConOSA X)] means ( S1[$1] & S2[$1] );
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
S3[t] ) holds
S3[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
S3[t] ) holds
S3[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
S3[t] ) implies S3[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] &
S2[
t] )
;
S3[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 A7:
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 x =
(PTClasses X) * ts as
FinSequence of
bool [:(TS (DTConOSA X)), the carrier of S:] ;
A8:
(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 ) ) ) }
;
reconsider ts1 =
ts as
Element of
Args (
o,
(ParsedTermsOSA X))
by A5;
set w =
the_arity_of o;
A9:
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 A9, FINSEQ_2:29;
then A10:
dom x = dom ts
by FINSEQ_3:29;
A11:
dom (the_arity_of o) = dom ts
by A5, MSUALG_3:6;
A12:
for
y being
Nat st
y in dom x holds
[(ts1 . y),((the_arity_of o) /. y)] in x . y
proof
let y be
Nat;
( y in dom x implies [(ts1 . y),((the_arity_of o) /. y)] in x . y )
assume A13:
y in dom x
;
[(ts1 . y),((the_arity_of o) /. y)] in x . y
A14:
ts1 . y in rng ts1
by A10, A13, FUNCT_1:3;
then reconsider t1 =
ts1 . y as
Element of
TS (DTConOSA X) by A9;
ts1 . y in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. y)
by A10, A11, A13, MSUALG_6:2;
then
[t1,((the_arity_of o) /. y)] in (PTClasses X) . t1
by A3, A14;
hence
[(ts1 . y),((the_arity_of o) /. y)] in x . y
by A10, A13, FUNCT_1:13;
verum
end;
thus
S1[
nt -tree ts]
S2[nt -tree ts]proof
let s1 be
Element of
S;
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff [(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts) )
assume
[(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts)
;
nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1
then consider o2 being
OperSymbol of
S,
x2 being
Element of
Args (
o2,
(ParsedTermsOSA X)),
s3 being
Element of
S such that A16:
[(nt -tree ts),s1] = [((Den (o2,(ParsedTermsOSA X))) . x2),s3]
and A17:
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
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 A8;
s1 = s3
by A16, XTUPLE_0:1;
then A18:
the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o2) c= the
Sorts of
(ParsedTermsOSA X) . s1
by A17, OSALG_1:def 16;
A19:
(Den (o2,(ParsedTermsOSA X))) . x2 in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o2)
by MSUALG_9:18;
nt -tree ts = (Den (o2,(ParsedTermsOSA X))) . x2
by A16, XTUPLE_0:1;
hence
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s1
by A19, A18;
verum
end;
thus
S2[
nt -tree ts]
verumproof
let s1 be
Element of
S;
for y being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (nt -tree ts) holds
[(nt -tree ts),s1] in (PTClasses X) . ylet y be
Element of
TS (DTConOSA X);
( [y,s1] in (PTClasses X) . (nt -tree ts) implies [(nt -tree ts),s1] in (PTClasses X) . y )
assume
[y,s1] in (PTClasses X) . (nt -tree ts)
;
[(nt -tree ts),s1] in (PTClasses X) . y
then consider o2 being
OperSymbol of
S,
x2 being
Element of
Args (
o2,
(ParsedTermsOSA X)),
s3 being
Element of
S such that A20:
[y,s1] = [((Den (o2,(ParsedTermsOSA X))) . x2),s3]
and A21:
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 A22:
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 A8;
consider w3 being
Element of the
carrier of
S * such that A23:
dom w3 = dom x
and A24:
for
y being
Nat st
y in dom x holds
[(x2 . y),(w3 /. y)] in x . y
by A22;
consider o1 being
OperSymbol of
S such that A25:
nt = [o1, the carrier of S]
and A26:
o1 ~= o2
and A27:
len (the_arity_of o1) = len (the_arity_of o2)
and A28:
the_result_sort_of o1 <= s3
and A29:
the_result_sort_of o2 <= s3
by A21;
A30:
y = (Den (o2,(ParsedTermsOSA X))) . x2
by A20, 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:] ;
A31:
OSSym (
o2,
X)
==> roots x2
by Th13;
then consider o3 being
OperSymbol of
S such that A32:
OSSym (
o2,
X)
= [o3, the carrier of S]
and
x3 in Args (
o3,
(ParsedTermsOSA X))
and A33:
(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 A32, XTUPLE_0:1;
then A34:
(PTClasses X) . y =
@ (
(OSSym (o2,X)),
xy)
by A30, A31, A33, 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 ) ) ) }
;
A35:
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 A36:
dom x3 = dom xy
by FINSEQ_3:29;
A37:
o1 = o
by A4, A25, XTUPLE_0:1;
then A38:
dom (the_arity_of o2) = dom (the_arity_of o)
by A27, FINSEQ_3:29;
then A39:
dom w3 = dom xy
by A10, A11, A23, A36, MSUALG_3:6;
A40:
dom x2 = dom x
by A10, A11, A38, MSUALG_3:6;
A41:
for
y being
Nat st
y in dom xy holds
[(ts1 . y),(w3 /. y)] in xy . y
proof
let y be
Nat;
( y in dom xy implies [(ts1 . y),(w3 /. y)] in xy . y )
assume A42:
y in dom xy
;
[(ts1 . y),(w3 /. y)] in xy . y
A43:
ts1 . y in rng ts1
by A10, A23, A39, A42, FUNCT_1:3;
x2 . y in rng x3
by A36, A42, FUNCT_1:3;
then reconsider t1 =
ts1 . y,
t2 =
x2 . y as
Element of
TS (DTConOSA X) by A9, A35, A43;
[(x2 . y),(w3 /. y)] in x . y
by A24, A36, A40, A42;
then
[(x2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y)
by A10, A23, A39, A42, FUNCT_1:13;
then
[t1,(w3 /. y)] in (PTClasses X) . t2
by A3, A43;
hence
[(ts1 . y),(w3 /. y)] in xy . y
by A42, FUNCT_1:12;
verum
end;
A44:
the_result_sort_of o2 <= s1
by A20, A29, XTUPLE_0:1;
the_result_sort_of o <= s1
by A20, A28, A37, XTUPLE_0:1;
hence
[(nt -tree ts),s1] in (PTClasses X) . y
by A6, A26, A27, A37, A39, A41, A34, A44;
verum
end;
end;
A45:
for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S3[ root-tree s]
proof
let sy be
Symbol of
(DTConOSA X);
( sy in Terminals (DTConOSA X) implies S3[ root-tree sy] )
assume A46:
sy in Terminals (DTConOSA X)
;
S3[ root-tree sy]
reconsider sy1 =
sy as
Terminal of
(DTConOSA X) by A46;
consider s being
Element of
S,
x being
set such that A47:
x in X . s
and A48:
sy = [x,s]
by A46, Th4;
A49:
(PTClasses X) . (root-tree sy) =
@ sy
by A46, 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 ) }
;
root-tree sy1 in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }
by A47, A48;
then A50:
root-tree sy1 in the
Sorts of
(ParsedTermsOSA X) . s
by Th9;
thus
S1[
root-tree sy]
S2[ root-tree sy]proof
let s1 be
Element of
S;
( root-tree sy in the Sorts of (ParsedTermsOSA X) . s1 iff [(root-tree sy),s1] in (PTClasses X) . (root-tree sy) )
assume
[(root-tree sy),s1] in (PTClasses X) . (root-tree sy)
;
root-tree sy in the Sorts of (ParsedTermsOSA X) . s1
then consider s3 being
Element of
S such that A51:
[(root-tree sy),s1] = [(root-tree sy),s3]
and A52:
ex
s2 being
Element of
S ex
x being
set st
(
x in X . s2 &
sy = [x,s2] &
s2 <= s3 )
by A49;
A53:
s1 = s3
by A51, XTUPLE_0:1;
consider s2 being
Element of
S,
x2 being
set such that
x2 in X . s2
and A54:
sy = [x2,s2]
and A55:
s2 <= s3
by A52;
s2 = s
by A48, A54, XTUPLE_0:1;
then
the
Sorts of
(ParsedTermsOSA X) . s c= the
Sorts of
(ParsedTermsOSA X) . s1
by A53, A55, OSALG_1:def 16;
hence
root-tree sy in the
Sorts of
(ParsedTermsOSA X) . s1
by A50;
verum
end;
thus
S2[
root-tree sy]
verumproof
let s1 be
Element of
S;
for y being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (root-tree sy) holds
[(root-tree sy),s1] in (PTClasses X) . ylet y be
Element of
TS (DTConOSA X);
( [y,s1] in (PTClasses X) . (root-tree sy) implies [(root-tree sy),s1] in (PTClasses X) . y )
assume A56:
[y,s1] in (PTClasses X) . (root-tree sy)
;
[(root-tree sy),s1] in (PTClasses X) . y
then
ex
s2 being
Element of
S st
(
[y,s1] = [(root-tree sy),s2] & ex
s3 being
Element of
S ex
x being
set st
(
x in X . s3 &
sy = [x,s3] &
s3 <= s2 ) )
by A49;
then
y = root-tree sy
by XTUPLE_0:1;
hence
[(root-tree sy),s1] in (PTClasses X) . y
by A56;
verum
end;
end;
for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S3[t]
from DTCONSTR:sch 7(A45, A1);
hence
( ( for s being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S
for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . y ) )
; verum