let S be locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
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 S₁[ 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
S₁[t] ) holds
S₁[nt -tree ts]

proof

let nt be Symbol of (DTConOSA X); :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
A2: nt ==> roots ts and
for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₁[t] ; :: thesis:
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; :: thesis:
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; :: thesis:
assume A12: y in dom x ; :: thesis:
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; :: thesis:

end;

assume ex y being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (nt -tree ts) ; :: thesis:
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; :: thesis:

end;

A17: for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S₁[ root-tree s]

proof

let sy be Symbol of (DTConOSA X); :: thesis:
assume sy in Terminals (DTConOSA X) ; :: thesis:
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; :: thesis:
assume ex y being Element of TS (DTConOSA X) st [y,s1] in (PTClasses X) . (root-tree sy) ; :: thesis:
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; :: thesis:

end;

for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S₁[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 ; :: thesis: