let S be locally_directed OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: 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
for y, z being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . $1 & [z,s] in (PTClasses X) . y holds
[$1,s] in (PTClasses X) . z;
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:
A3: (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:
let y, z be Element of TS (DTConOSA X); :: thesis:
assume A4: ( [y,s1] in (PTClasses X) . (root-tree sy) & [z,s1] in (PTClasses X) . y ) ; :: thesis:
then consider s2 being Element of S such that
A5: [y,s1] = [(root-tree sy),s2] and
ex s0 being Element of S ex x being set st
( x in X . s0 & sy = [x,s0] & s0 <= s2 ) by A3;
A6: ( y = root-tree sy & s1 = s2 ) by A5, ZFMISC_1:33;
then consider s3 being Element of S such that
A7: [z,s1] = [(root-tree sy),s3] and
ex s0 being Element of S ex x being set st
( x in X . s0 & sy = [x,s0] & s0 <= s3 ) by A3, A4;
thus [(root-tree sy),s1] in (PTClasses X) . z by A4, A6, A7, ZFMISC_1:33; :: thesis:

end;

A8: 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
A9: nt ==> roots ts and
A10: for t being DecoratedTree of st t in rng ts holds
S₁[t] ; :: thesis:
consider o being OperSymbol of S such that
A11: ( 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 A9, Th12;
reconsider ts1 = ts as Element of Args o,(ParsedTermsOSA X) by A11;
set w = the_arity_of o;
reconsider x = (PTClasses X) * ts as FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] ;
A12: ( 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 A13: ( dom x = dom ts & dom (the_arity_of o) = dom ts ) by A11, FINSEQ_3:31, MSUALG_3:6;
A14: (PTClasses X) . (nt -tree ts) = @ nt,x by A9, 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:
let y, z be Element of TS (DTConOSA X); :: thesis:
assume A15: ( [y,s1] in (PTClasses X) . (nt -tree ts) & [z,s1] in (PTClasses X) . y ) ; :: thesis:
then consider o2 being OperSymbol of S, x2 being Element of Args o2,(ParsedTermsOSA X), s3 being Element of S such that
A16: [y,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 ) & 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 A14;
A18: ( y = (Den o2,(ParsedTermsOSA X)) . x2 & s1 = s3 ) by A16, ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A19: ( 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 A17;
A20: o1 = o by A11, A19, ZFMISC_1:33;
A21: ( 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
A22: ( 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 A21, Th12;
A23: o2 = o3 by A22, ZFMISC_1:33;
A24: dom (the_arity_of o2) = dom (the_arity_of o) by A19, A20, FINSEQ_3:31;
consider w3 being Element of the carrier of S * such that
A25: ( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) by A17;
reconsider xy = (PTClasses X) * x3 as FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] ;
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 A26: dom x3 = dom xy by FINSEQ_3:31;
A27: dom x2 = dom x by A13, A24, MSUALG_3:6;
(PTClasses X) . y = @ (OSSym o2,X),xy by A18, A21, A22, A23, 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 ) ) ) } ;
then consider o5 being OperSymbol of S, x5 being Element of Args o5,(ParsedTermsOSA X), s5 being Element of S such that
A28: [z,s1] = [((Den o5,(ParsedTermsOSA X)) . x5),s5] and
A29: ( ex o1 being OperSymbol of S st
( OSSym o2,X = [o1,the carrier of S] & o1 ~= o5 & len (the_arity_of o1) = len (the_arity_of o5) & the_result_sort_of o1 <= s5 & the_result_sort_of o5 <= s5 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom xy & ( for y being Nat st y in dom xy holds
[(x5 . y),(w3 /. y)] in xy . y ) ) ) by A15;
A30: ( z = (Den o5,(ParsedTermsOSA X)) . x5 & s1 = s5 ) by A28, ZFMISC_1:33;
consider o6 being OperSymbol of S such that
A31: ( OSSym o2,X = [o6,the carrier of S] & o6 ~= o5 & len (the_arity_of o6) = len (the_arity_of o5) & the_result_sort_of o6 <= s5 & the_result_sort_of o5 <= s5 ) by A29;
A32: o6 = o2 by A31, ZFMISC_1:33;
A33: ( x5 is FinSequence of TS (DTConOSA X) & OSSym o5,X ==> roots x5 ) by Th13;
reconsider x6 = x5 as FinSequence of TS (DTConOSA X) by Th13;
consider o7 being OperSymbol of S such that
A34: ( OSSym o5,X = [o7,the carrier of S] & x6 in Args o7,(ParsedTermsOSA X) & (OSSym o5,X) -tree x6 = (Den o7,(ParsedTermsOSA X)) . x6 & ( for s2 being Element of S holds
( (OSSym o5,X) -tree x6 in the Sorts of (ParsedTermsOSA X) . s2 iff the_result_sort_of o7 <= s2 ) ) ) by A33, Th12;
A35: o5 = o7 by A34, ZFMISC_1:33;
A36: dom (the_arity_of o5) = dom (the_arity_of o2) by A31, A32, FINSEQ_3:31;
consider w5 being Element of the carrier of S * such that
A37: ( dom w5 = dom xy & ( for y being Nat st y in dom xy holds
[(x5 . y),(w5 /. y)] in xy . y ) ) by A29;
reconsider xz = (PTClasses X) * x6 as FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] ;
A38: ( rng x6 c= TS (DTConOSA X) & rng x3 c= TS (DTConOSA X) ) by FINSEQ_1:def 4;
then rng x6 c= dom (PTClasses X) by FUNCT_2:def 1;
then len xz = len x6 by FINSEQ_2:33;
then A39: dom x6 = dom xz by FINSEQ_3:31;
A40: dom x5 = dom (the_arity_of o2) by A36, MSUALG_3:6
.= dom xy by A26, MSUALG_3:6 ;
defpred S₂[ set , set ] means [(ts1 . $1),$2] in xz . $1;
A41: for y being set st y in dom xz holds
ex sy being set st
( sy in the carrier of S & S₂[y,sy] )

proof

let y be set ; :: thesis:
assume A42: y in dom xz ; :: thesis:
A43: ( y in dom ts1 & y in dom x5 & y in dom x2 & y in dom x ) by A13, A24, A26, A39, A40, A42, MSUALG_3:6;
( ts1 . y in rng ts1 & x5 . y in rng x6 & x2 . y in rng x3 ) by A13, A26, A27, A39, A40, A42, FUNCT_1:12;
then reconsider t1 = ts1 . y, t2 = x3 . y, t3 = x5 . y as Element of TS (DTConOSA X) by A12, A38;
[(x5 . y),(w5 /. y)] in xy . y by A37, A39, A40, A42;
then A45: [t3,(w5 /. y)] in (PTClasses X) . t2 by A26, A39, A40, A42, FUNCT_1:23;
then A46: ( [t2,(w5 /. y)] in (PTClasses X) . t2 & [t2,(w5 /. y)] in (PTClasses X) . t3 ) by Th20, Th21;
then [t3,(w5 /. y)] in (PTClasses X) . t3 by Th21;
then A47: ( t2 in the Sorts of (ParsedTermsOSA X) . (w5 /. y) & t3 in the Sorts of (ParsedTermsOSA X) . (w5 /. y) ) by A46, Th20;
then A48: LeastSort t2 <= w5 /. y by Def12;
A49: [(x2 . y),(w3 /. y)] in x . y by A25, A26, A27, A39, A40, A42;
then A50: [(x2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y) by A13, A26, A27, A39, A40, A42, FUNCT_1:23;
[t2,(w3 /. y)] in (PTClasses X) . t1 by A43, A49, FUNCT_1:23;
then A51: ( [t1,(w3 /. y)] in (PTClasses X) . t2 & [t1,(w3 /. y)] in (PTClasses X) . t1 ) by Th20, Th21;
then [t2,(w3 /. y)] in (PTClasses X) . t2 by Th21;
then A52: ( t2 in the Sorts of (ParsedTermsOSA X) . (w3 /. y) & t1 in the Sorts of (ParsedTermsOSA X) . (w3 /. y) ) by A51, Th20;
then LeastSort t2 <= w3 /. y by Def12;
then consider s7 being Element of S such that
A53: ( w5 /. y <= s7 & w3 /. y <= s7 ) by A48, OSALG_4:12;
A54: [t2,s7] in (PTClasses X) . t1 by A50, A52, A53, Th22;
[t3,s7] in (PTClasses X) . t2 by A45, A47, A53, Th22;
then A55: [t1,s7] in (PTClasses X) . t3 by A10, A13, A26, A27, A39, A40, A42, A54, FUNCT_1:12;
take s7 ; :: thesis:
thus s7 in the carrier of S ; :: thesis:
thus S₂[y,s7] by A42, A55, FUNCT_1:22; :: thesis:

end;

consider f being Function of (dom xz),the carrier of S such that
A56: for y being set st y in dom xz holds
S₂[y,f . y] from FUNCT_2:sch 1(A41);
A57: dom f = dom xz by FUNCT_2:def 1;
then ex n being Nat st dom f = Seg n by FINSEQ_1:def 2;
then reconsider f1 = f as FinSequence by FINSEQ_1:def 2;
rng f c= the carrier of S by RELAT_1:def 19;
then f1 is FinSequence of the carrier of S by FINSEQ_1:def 4;
then reconsider f = f as Element of the carrier of S * by FINSEQ_1:def 11;
A58: ( dom f = dom xz & ( for y being Nat st y in dom xz holds
[(ts1 . y),(f /. y)] in xz . y ) )

proof

thus dom f = dom xz by FUNCT_2:def 1; :: thesis:
let y be Nat; :: thesis:
assume A59: y in dom xz ; :: thesis:
[(ts1 . y),(f . y)] in xz . y by A56, A59;
hence [(ts1 . y),(f /. y)] in xz . y by A57, A59, PARTFUN1:def 8; :: thesis:

end;

A60: (PTClasses X) . z = @ (OSSym o5,X),xz by A30, A33, A34, A35, 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 o5,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 xz & ( for y being Nat st y in dom xz holds
[(x4 . y),(w4 /. y)] in xz . y ) ) ) } ;
( OSSym o5,X = [o5,the carrier of S] & o5 ~= o & len (the_arity_of o5) = len (the_arity_of o) & the_result_sort_of o5 <= s1 & the_result_sort_of o <= s1 ) by A16, A19, A20, A28, A31, A32, OSALG_1:2, ZFMISC_1:33;
hence [(nt -tree ts),s1] in (PTClasses X) . z by A11, A58, A60; :: thesis:

end;

for t being DecoratedTree of st t in TS (DTConOSA X) holds
S₁[t] from DTCONSTR:sch 7(A1, A8);
hence for x, y, z being Element of TS (DTConOSA X)
for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds
[x,s] in (PTClasses X) . z ; :: thesis: