let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for t being Element of TS (DTConOSA X)
for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . t
let X be V2() ManySortedSet of S; for t being Element of TS (DTConOSA X)
for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . t
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 st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . $1 holds
[$1,s] in (PTClasses X) . $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
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
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 A3:
nt = [o, the carrier of S]
and A4:
ts in Args (
o,
(ParsedTermsOSA X))
and A5:
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 x =
(PTClasses X) * ts as
FinSequence of
bool [:(TS (DTConOSA X)), the carrier of S:] ;
A6:
(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 A4;
set w =
the_arity_of o;
A7:
len (the_arity_of o) = len (the_arity_of o)
;
let s1 be
Element of
S;
( ex y being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (nt -tree ts) implies [(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts) )
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:
dom (the_arity_of o) = dom ts
by A4, MSUALG_3:6;
A11:
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 A12:
y in dom x
;
[(ts1 . y),((the_arity_of o) /. y)] in x . y
ts1 . y in rng ts1
by A9, A12, FUNCT_1:3;
then reconsider t1 =
ts1 . y as
Element of
TS (DTConOSA X) by A8;
ts1 . y in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. y)
by A9, A10, A12, MSUALG_6:2;
then
[t1,((the_arity_of o) /. y)] in (PTClasses X) . t1
by Th19;
hence
[(ts1 . y),((the_arity_of o) /. y)] in x . y
by A9, A12, FUNCT_1:13;
verum
end;
assume
ex
y being
Element of
TS (DTConOSA X) st
[y,s1] in (PTClasses X) . (nt -tree ts)
;
[(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts)
then consider y being
Element of
TS (DTConOSA X) such that A13:
[y,s1] in (PTClasses X) . (nt -tree ts)
;
consider o2 being
OperSymbol of
S,
x2 being
Element of
Args (
o2,
(ParsedTermsOSA X)),
s3 being
Element of
S such that A14:
[y,s1] = [((Den (o2,(ParsedTermsOSA X))) . x2),s3]
and A15:
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 A6, A13;
A16:
s1 = s3
by A14, XTUPLE_0:1;
the_result_sort_of o <= s3
by A3, A15, XTUPLE_0:1;
hence
[(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts)
by A3, A5, A9, A10, A11, A6, A16, A7;
verum
end;
A17:
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 A18:
(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 ) }
;
let s1 be
Element of
S;
( ex y being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (root-tree sy) implies [(root-tree sy),s1] in (PTClasses X) . (root-tree sy) )
assume
ex
y being
Element of
TS (DTConOSA X) st
[y,s1] in (PTClasses X) . (root-tree sy)
;
[(root-tree sy),s1] in (PTClasses X) . (root-tree sy)
then consider y being
Element of
TS (DTConOSA X) such that A19:
[y,s1] in (PTClasses X) . (root-tree sy)
;
ex
s3 being
Element of
S st
(
[y,s1] = [(root-tree sy),s3] & ex
s2 being
Element of
S ex
x being
set st
(
x in X . s2 &
sy = [x,s2] &
s2 <= s3 ) )
by A18, A19;
hence
[(root-tree sy),s1] in (PTClasses X) . (root-tree sy)
by A19, XTUPLE_0:1;
verum
end;
for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S1[t]
from DTCONSTR:sch 7(A17, A1);
hence
for t being Element of TS (DTConOSA X)
for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . t
; verum