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

proof

end;

consider f being Function of (dom xz), the carrier of S such that
A63: for y being object st y in dom xz holds
S₂[y,f . y] from FUNCT_2:sch 1(A49);
A64: 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;
A65: ( 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 A66: y in dom xz ; :: thesis:
[(ts1 . y),(f . y)] in xz . y by A63, A66;
hence [(ts1 . y),(f /. y)] in xz . y by A64, A66, PARTFUN1:def 6; :: thesis:

end;

o5 ~= o by A37, A40, A24, A46, OSALG_1:2;
hence [(nt -tree ts),s1] in (PTClasses X) . z by A6, A38, A40, A25, A46, A65, A35, A27, A41; :: thesis:

end;

A67: 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 A68: (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 ) } ;
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 that
A69: [y,s1] in (PTClasses X) . (root-tree sy) and
A70: [z,s1] in (PTClasses X) . y ; :: thesis:
ex s2 being Element of S st
( [y,s1] = [(root-tree sy),s2] & ex s0 being Element of S ex x being set st
( x in X . s0 & sy = [x,s0] & s0 <= s2 ) ) by A68, A69;
then A71: y = root-tree sy by XTUPLE_0:1;
then ex s3 being Element of S st
( [z,s1] = [(root-tree sy),s3] & ex s0 being Element of S ex x being set st
( x in X . s0 & sy = [x,s0] & s0 <= s3 ) ) by A68, A70;
hence [(root-tree sy),s1] in (PTClasses X) . z by A69, A71, 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(A67, A1);
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: