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 s1, s2 being Element of S
for y being Element of TS (DTConOSA X) st s1 <= s2 & $1 in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [y,s1] in (PTClasses X) . $1 iff [y,s2] 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
ts in Args (o,(ParsedTermsOSA X)) and
nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts and
A4: 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:] ;
let s1, s2 be Element of S; :: thesis:
let y be Element of TS (DTConOSA X); :: thesis:
assume that
A5: s1 <= s2 and
A6: nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 and
A7: y in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis:
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 ) ) ) } ;

hereby :: thesis:

reconsider s21 = s2 as Element of S ;
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
A9: [y,s1] = [((Den (o2,(ParsedTermsOSA X))) . x2),s3] and
A10: 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
A11: 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 o1 being OperSymbol of S such that
A12: nt = [o1, the carrier of S] and
A13: o1 ~= o2 and
A14: len (the_arity_of o1) = len (the_arity_of o2) and
A15: the_result_sort_of o1 <= s3 and
A16: the_result_sort_of o2 <= s3 by A10;
A17: y = (Den (o2,(ParsedTermsOSA X))) . x2 by A9, XTUPLE_0:1;
A18: s1 = s3 by A9, XTUPLE_0:1;
then A19: the_result_sort_of o2 <= s21 by A5, A16, ORDERS_2:3;
the_result_sort_of o1 <= s21 by A5, A18, A15, ORDERS_2:3;
hence [y,s2] in (PTClasses X) . (nt -tree ts) by A8, A11, A17, A12, A13, A14, A19; :: thesis:

end;

assume [y,s2] 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
A20: [y,s2] = [((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;
reconsider x3 = x2 as FinSequence of TS (DTConOSA X) by Th13;
OSSym (o2,X) ==> roots x2 by Th13;
then consider o3 being OperSymbol of S such that
A23: OSSym (o2,X) = [o3, the carrier of S] and
x3 in Args (o3,(ParsedTermsOSA X)) and
A24: (OSSym (o2,X)) -tree x3 = (Den (o3,(ParsedTermsOSA X))) . x3 and
A25: 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;
A26: y = (Den (o2,(ParsedTermsOSA X))) . x2 by A20, XTUPLE_0:1;
o2 = o3 by A23, XTUPLE_0:1;
then A27: the_result_sort_of o2 <= s1 by A7, A26, A24, A25;
consider o1 being OperSymbol of S such that
A28: nt = [o1, the carrier of S] and
A29: o1 ~= o2 and
A30: len (the_arity_of o1) = len (the_arity_of o2) and
the_result_sort_of o1 <= s3 and
the_result_sort_of o2 <= s3 by A21;
the_result_sort_of o <= s1 by A4, A6;
then the_result_sort_of o1 <= s1 by A3, A28, XTUPLE_0:1;
hence [y,s1] in (PTClasses X) . (nt -tree ts) by A8, A22, A26, A28, A29, A30, A27; :: thesis:

end;

A31: 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 A32: sy in Terminals (DTConOSA X) ; :: thesis:
reconsider sy1 = sy as Terminal of (DTConOSA X) by A32;
A33: (PTClasses X) . (root-tree sy) = @ sy by A32, 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, s2 be Element of S; :: thesis:
let y be Element of TS (DTConOSA X); :: thesis:
assume that
A34: s1 <= s2 and
A35: root-tree sy in the Sorts of (ParsedTermsOSA X) . s1 and
y in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis:
the Sorts of (ParsedTermsOSA X) . s1 c= the Sorts of (ParsedTermsOSA X) . s2 by A34, OSALG_1:def 16;
then A36: [(root-tree sy1),s2] in (PTClasses X) . (root-tree sy) by A35, Th19;

hereby :: thesis:

assume [y,s1] in (PTClasses X) . (root-tree sy) ; :: thesis:
then 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 A33;
hence [y,s2] in (PTClasses X) . (root-tree sy) by A36, XTUPLE_0:1; :: thesis:

end;

assume [y,s2] in (PTClasses X) . (root-tree sy) ; :: thesis:
then A37: ex s3 being Element of S st
( [y,s2] = [(root-tree sy),s3] & ex s4 being Element of S ex x being set st
( x in X . s4 & sy = [x,s4] & s4 <= s3 ) ) by A33;
[(root-tree sy1),s1] in (PTClasses X) . (root-tree sy) by A35, Th19;
hence [y,s1] in (PTClasses X) . (root-tree sy) by A37, 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(A31, A1);
hence for x, y being Element of TS (DTConOSA X)
for s1, s2 being Element of S st s1 <= s2 & x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [y,s1] in (PTClasses X) . x iff [y,s2] in (PTClasses X) . x ) ; :: thesis: