let S be locally_directed OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: thesis:
let t be Element of TS (DTConOSA X); :: thesis:
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 S₁[ 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 S₂[ 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 S₃[ DecoratedTree of ] means ( S₁[$1] & S₂[$1] );
A1: 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 A2: sy in Terminals (DTConOSA X) ; :: thesis:
reconsider sy1 = sy as Terminal of (DTConOSA X) by A2;
consider s being Element of S, x being set such that
A3: ( x in X . s & sy = [x,s] ) by A2, Th4;
root-tree sy1 in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set 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 A3;
then A4: root-tree sy1 in the Sorts of (ParsedTermsOSA X) . s by Th9;
A5: (PTClasses X) . (root-tree sy) = @ sy by A2, Def22
.= { [(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 S₁[ root-tree sy] :: thesis:

proof

let s1 be Element of S; :: thesis:

hereby :: thesis:

assume root-tree sy in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis:
then s <= s1 by A3, Th10;
hence [(root-tree sy),s1] in (PTClasses X) . (root-tree sy) by A3, A5; :: thesis:

end;

assume [(root-tree sy),s1] in (PTClasses X) . (root-tree sy) ; :: thesis:
then consider s3 being Element of S such that
A6: [(root-tree sy),s1] = [(root-tree sy),s3] and
A7: ex s2 being Element of S ex x being set st
( x in X . s2 & sy = [x,s2] & s2 <= s3 ) by A5;
A8: s1 = s3 by A6, ZFMISC_1:33;
consider s2 being Element of S, x2 being set such that
A9: ( x2 in X . s2 & sy = [x2,s2] & s2 <= s3 ) by A7;
( x2 = x & s2 = s ) by A3, A9, ZFMISC_1:33;
then the Sorts of (ParsedTermsOSA X) . s c= the Sorts of (ParsedTermsOSA X) . s1 by A8, A9, OSALG_1:def 18;
hence root-tree sy in the Sorts of (ParsedTermsOSA X) . s1 by A4; :: thesis:

end;

thus S₂[ root-tree sy] :: thesis:

proof

let s1 be Element of S; :: thesis:
let y be Element of TS (DTConOSA X); :: thesis:
assume A10: [y,s1] in (PTClasses X) . (root-tree sy) ; :: thesis:
then consider s2 being Element of S such that
A11: [y,s1] = [(root-tree sy),s2] and
ex s3 being Element of S ex x being set st
( x in X . s3 & sy = [x,s3] & s3 <= s2 ) by A5;
( y = root-tree sy & s1 = s2 ) by A11, ZFMISC_1:33;
hence [(root-tree sy),s1] in (PTClasses X) . y by A10; :: thesis:

end;

A12: for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of 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
A13: nt ==> roots ts and
A14: for t being DecoratedTree of st t in rng ts holds
( S₁[t] & S₂[t] ) ; :: thesis:
consider o being OperSymbol of S such that
A15: ( nt = [o,the carrier of S] & ts in Args o,(ParsedTermsOSA X) & nt -tree ts = (Den o,(ParsedTermsOSA X)) . ts & ( 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 A13, Th12;
reconsider ts1 = ts as Element of Args o,(ParsedTermsOSA X) by A15;
set w = the_arity_of o;
reconsider x = (PTClasses X) * ts as FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] ;
A16: ( rng ts c= TS (DTConOSA X) & dom (PTClasses X) = TS (DTConOSA X) ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then len x = len ts by FINSEQ_2:33;
then A17: ( dom x = dom ts & dom (the_arity_of o) = dom ts ) by A15, FINSEQ_3:31, MSUALG_3:6;
A18: 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 A19: y in dom x ; :: thesis:
A20: ts1 . y in rng ts1 by A17, A19, FUNCT_1:12;
then reconsider t1 = ts1 . y as Element of TS (DTConOSA X) by A16;
ts1 . y in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. y) by A17, A19, MSUALG_6:2;
then [t1,((the_arity_of o) /. y)] in (PTClasses X) . t1 by A14, A20;
hence [(ts1 . y),((the_arity_of o) /. y)] in x . y by A17, A19, FUNCT_1:23; :: thesis:

end;

A21: (PTClasses X) . (nt -tree ts) = @ nt,x by A13, Def22
.= { [((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 S₁[nt -tree ts] :: thesis:

proof

let s1 be Element of S; :: thesis:

hereby :: thesis:

assume nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis:
then ( o ~= o & len (the_arity_of o) = len (the_arity_of o) & the_result_sort_of o <= s1 & the_result_sort_of o <= s1 ) by A15;
hence [(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts) by A15, A17, A18, A21; :: thesis:

end;

assume [(nt -tree ts),s1] in (PTClasses X) . (nt -tree ts) ; :: thesis:
then consider o2 being OperSymbol of S, x2 being Element of Args o2,(ParsedTermsOSA X), s3 being Element of S such that
A22: [(nt -tree ts),s1] = [((Den o2,(ParsedTermsOSA X)) . x2),s3] and
A23: ( 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 ) ) ) by A21;
A24: ( nt -tree ts = (Den o2,(ParsedTermsOSA X)) . x2 & s1 = s3 ) by A22, ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A25: ( 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 ) by A23;
A26: (Den o2,(ParsedTermsOSA X)) . x2 in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) by MSUALG_9:19;
the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) c= the Sorts of (ParsedTermsOSA X) . s1 by A24, A25, OSALG_1:def 18;
hence nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 by A24, A26; :: thesis:

end;

thus S₂[nt -tree ts] :: thesis:

proof

let s1 be Element of S; :: thesis:
let y be Element of TS (DTConOSA X); :: thesis:
assume [y,s1] in (PTClasses X) . (nt -tree ts) ; :: thesis:
then consider o2 being OperSymbol of S, x2 being Element of Args o2,(ParsedTermsOSA X), s3 being Element of S such that
A27: [y,s1] = [((Den o2,(ParsedTermsOSA X)) . x2),s3] and
A28: ( 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 ) ) ) by A21;
A29: ( y = (Den o2,(ParsedTermsOSA X)) . x2 & s1 = s3 ) by A27, ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A30: ( 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 ) by A28;
A31: o1 = o by A15, A30, ZFMISC_1:33;
A32: ( x2 is FinSequence of TS (DTConOSA X) & OSSym o2,X ==> roots x2 ) by Th13;
reconsider x3 = x2 as FinSequence of TS (DTConOSA X) by Th13;
consider o3 being OperSymbol of S such that
A33: ( OSSym o2,X = [o3,the carrier of S] & x3 in Args o3,(ParsedTermsOSA X) & (OSSym o2,X) -tree x3 = (Den o3,(ParsedTermsOSA X)) . x3 & ( 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 A32, Th12;
A34: o2 = o3 by A33, ZFMISC_1:33;
A35: dom (the_arity_of o2) = dom (the_arity_of o) by A30, A31, FINSEQ_3:31;
consider w3 being Element of the carrier of S * such that
A36: ( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) by A28;
reconsider xy = (PTClasses X) * x3 as FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] ;
A37: 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:33;
then A38: dom x3 = dom xy by FINSEQ_3:31;
A39: dom x2 = dom x by A17, A35, MSUALG_3:6;
A40: ( dom w3 = dom xy & dom xy = dom x3 ) by A17, A35, A36, 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; :: thesis:
assume A42: y in dom xy ; :: thesis:
A43: ( ts1 . y in rng ts1 & x2 . y in rng x3 ) by A17, A36, A40, A42, FUNCT_1:12;
then reconsider t1 = ts1 . y, t2 = x2 . y as Element of TS (DTConOSA X) by A16, A37;
[(x2 . y),(w3 /. y)] in x . y by A36, A38, A39, A42;
then [(x2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y) by A17, A36, A40, A42, FUNCT_1:23;
then [t1,(w3 /. y)] in (PTClasses X) . t2 by A14, A43;
hence [(ts1 . y),(w3 /. y)] in xy . y by A42, FUNCT_1:22; :: thesis:

end;

A44: (PTClasses X) . y = @ (OSSym o2,X),xy by A29, A32, A33, A34, Def22
.= { [((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 ) ) ) } ;
( OSSym o2,X = [o2,the carrier of S] & o2 ~= o & len (the_arity_of o2) = len (the_arity_of o) & the_result_sort_of o2 <= s1 & the_result_sort_of o <= s1 ) by A27, A30, A31, ZFMISC_1:33;
hence [(nt -tree ts),s1] in (PTClasses X) . y by A15, A40, A41, A44; :: thesis:

end;

for t being DecoratedTree of st t in TS (DTConOSA X) holds
S₃[t] from DTCONSTR:sch 7(A1, A12);
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 ) ) ; :: thesis: