let S be monotone regular locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let t be Element of TS (DTConOSA X); :: thesis:
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
set R = PTCongruence X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set M = PTMin X;
set F = PTClasses X;
defpred S₁[ Element of TS (DTConOSA X)] means (PTMin X) . $1 in OSClass ((PTCongruence X),$1);
defpred S₂[ Element of TS (DTConOSA X)] means LeastSort ((PTMin X) . $1) <= LeastSort $1;
defpred S₃[ Element of TS (DTConOSA X)] means for s being Element of S
for x being set st x in X . s & $1 = root-tree [x,s] holds
(PTMin X) . $1 = $1;
defpred S₄[ Element of TS (DTConOSA X)] means for o being OperSymbol of S
for ts being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots ts & $1 = (OSSym (o,X)) -tree ts holds
( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym (o,X) ==> roots ((PTMin X) * ts) & OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) & (PTMin X) . $1 = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) );
defpred S₅[ DecoratedTree of the carrier of (DTConOSA X)] means ex t1 being Element of TS (DTConOSA X) st
( t1 = $1 & S₁[t1] & S₂[t1] & S₃[t1] & S₄[t1] );
A1: for nt being Symbol of (DTConOSA X)
for ts1 being FinSequence of TS (DTConOSA X) st nt ==> roots ts1 & ( for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S₅[dt1] ) holds
S₅[nt -tree ts1]

proof

let nt be Symbol of (DTConOSA X); :: thesis:
let ts1 be FinSequence of TS (DTConOSA X); :: thesis:
assume that
A2: nt ==> roots ts1 and
A3: for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
ex t2 being Element of TS (DTConOSA X) st
( t2 = dt1 & S₁[t2] & S₂[t2] & S₃[t2] & S₄[t2] ) ; :: thesis:
reconsider t1 = nt -tree ts1 as Element of TS (DTConOSA X) by A2, Th12;
A4: rng ts1 c= TS (DTConOSA X) by FINSEQ_1:def 4;
consider o being OperSymbol of S such that
A5: nt = [o, the carrier of S] and
A6: ts1 in Args (o,(ParsedTermsOSA X)) and
A7: nt -tree ts1 = (Den (o,(ParsedTermsOSA X))) . ts1 and
for s1 being Element of S holds
( nt -tree ts1 in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) by A2, Th12;
set Ms = (PTMin X) * ts1;
set LSMs = LeastSorts ((PTMin X) * ts1);
set w = the_arity_of o;
set so = the_result_sort_of o;
set Lo = LBound (o,(LeastSorts ((PTMin X) * ts1)));
A8: dom ts1 = dom (the_arity_of o) by A6, MSUALG_3:6;
A9: dom ((PTMin X) * ts1) = dom ts1 by FINSEQ_3:120;
then A10: dom (LeastSorts ((PTMin X) * ts1)) = dom ts1 by Def13;
@ (X,nt) = o by A2, A5, Def15;
then A11: (PTMin X) . (nt -tree ts1) = pi (o,((PTMin X) * ts1)) by A2, Def31;
A12: S₄[t1]

proof

let o2 be OperSymbol of S; :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
OSSym (o2,X) ==> roots ts and
A13: t1 = (OSSym (o2,X)) -tree ts ; :: thesis:
set Ms1 = (PTMin X) * ts;
set LSMs1 = LeastSorts ((PTMin X) * ts);
set Lo2 = LBound (o2,(LeastSorts ((PTMin X) * ts)));
A14: ts = ts1 by A13, TREES_4:15;
A15: OSSym (o2,X) = nt by A13, TREES_4:15;
then A16: o2 = o by A5, XTUPLE_0:1;
A17: LeastSorts ((PTMin X) * ts1) <= the_arity_of o

proof

thus len (LeastSorts ((PTMin X) * ts1)) = len (the_arity_of o) by A8, A10, FINSEQ_3:29; :: according to OSALG_1:def 6 :: thesis:
let i be set ; :: thesis:
assume A18: i in dom (LeastSorts ((PTMin X) * ts1)) ; :: thesis:
reconsider k = i as Nat by A18;
ts1 . k in rng ts1 by A10, A18, FUNCT_1:3;
then reconsider tr = ts1 . k as Element of TS (DTConOSA X) by A4;
A19: ex tr1 being Element of TS (DTConOSA X) st
( tr1 = tr & S₁[tr1] & S₂[tr1] & S₃[tr1] & S₄[tr1] ) by A3, A10, A18, FUNCT_1:3;
A20: (the_arity_of o) /. k = (the_arity_of o) . i by A8, A10, A18, PARTFUN1:def 6;
A21: ((PTMin X) * ts1) . k = (PTMin X) . tr by A9, A10, A18, FINSEQ_3:120;
ts1 . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k) by A6, A8, A10, A18, MSUALG_6:2;
then A22: LeastSort tr <= (the_arity_of o) /. k by Def12;
let s1, s2 be Element of S; :: thesis:
assume that
A23: s1 = (LeastSorts ((PTMin X) * ts1)) . i and
A24: s2 = (the_arity_of o) . i ; :: thesis:
ex t3 being Element of TS (DTConOSA X) st
( t3 = ((PTMin X) * ts1) . k & (LeastSorts ((PTMin X) * ts1)) . k = LeastSort t3 ) by A9, A10, A18, Def13;
hence s1 <= s2 by A19, A23, A24, A21, A22, A20, ORDERS_2:3; :: thesis:

end;

end;

A26: for s being Element of S
for x being set st x in X . s & t1 = root-tree [x,s] holds
(PTMin X) . t1 = t1

proof

let s be Element of S; :: thesis:
let x be set ; :: thesis:
assume that
A27: x in X . s and
A28: t1 = root-tree [x,s] ; :: thesis:
t1 . {} = [o, the carrier of S] by A5, TREES_4:def 4;
hence (PTMin X) . t1 = t1 by A27, A28, Th10; :: thesis:

end;

proof

defpred S₆[ object , object ] means [(((PTMin X) * ts1) . $1),$2] in ((PTClasses X) * ts1) . $1;
A46: for i being object st i in dom ((PTClasses X) * ts1) holds
ex s4 being object st
( s4 in the carrier of S & S₆[i,s4] )

proof

let i be object ; :: thesis:
assume A47: i in dom ((PTClasses X) * ts1) ; :: thesis:
A48: ((PTClasses X) * ts1) . i = (PTClasses X) . (ts1 . i) by A47, FINSEQ_3:120;
ts1 . i in rng ts1 by A31, A47, FUNCT_1:3;
then reconsider td1 = ts1 . i as Element of TS (DTConOSA X) by A4;
A49: ex td2 being Element of TS (DTConOSA X) st
( td2 = td1 & (PTMin X) . td2 in OSClass ((PTCongruence X),td2) & S₂[td2] & S₃[td2] & S₄[td2] ) by A3, A31, A47, FUNCT_1:3;
A50: ((PTMin X) * ts1) . i = (PTMin X) . (ts1 . i) by A31, A47, FUNCT_1:13;
reconsider tda = td1 as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort td1) by Def12;
OSClass ((PTCongruence X),td1) = OSClass ((PTCongruence X),tda) by Def27
.= proj1 (((PTClasses X) * ts1) . i) by A48, Th25 ;
then ex s4 being object st [(((PTMin X) * ts1) . i),s4] in ((PTClasses X) * ts1) . i by A50, A49, XTUPLE_0:def 12;
hence ex s4 being object st
( s4 in the carrier of S & S₆[i,s4] ) by A48, Th23; :: thesis:

end;

consider f being Function such that
A51: ( dom f = dom ((PTClasses X) * ts1) & rng f c= the carrier of S & ( for z being object st z in dom ((PTClasses X) * ts1) holds
S₆[z,f . z] ) ) from FUNCT_1:sch 6(A46);
reconsider wa = f as FinSequence by A31, A30, A51, FINSEQ_1:def 2;
reconsider wa = wa as FinSequence of the carrier of S by A51, FINSEQ_1:def 4;
reconsider wa = wa as Element of the carrier of S * by FINSEQ_1:def 11;
for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(Msr . y),(wa /. y)] in ((PTClasses X) * ts1) . y

proof

let y be Nat; :: thesis:
assume A52: y in dom ((PTClasses X) * ts1) ; :: thesis:
wa /. y = wa . y by A51, A52, PARTFUN1:def 6;
hence [(Msr . y),(wa /. y)] in ((PTClasses X) * ts1) . y by A51, A52; :: thesis:

end;

then [((Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . Msr),(the_result_sort_of o)] in (PTClasses X) . t1 by A5, A29, A41, A44, A42, A51;
hence (PTMin X) . t1 in OSClass ((PTCongruence X),t1) by A43, A37, XTUPLE_0:def 12; :: thesis:

end;

(PTMin X) . t1 = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),X)) -tree ((PTMin X) * ts1) by A2, A32, A12;
then A53: LeastSort ((PTMin X) . t1) = the_result_sort_of (LBound (o,(LeastSorts ((PTMin X) * ts1)))) by A34, A35, A36, Th17;
LeastSort t1 = the_result_sort_of o by A6, A7, Th17;
hence ( S₁[t1] & S₂[t1] & S₃[t1] & S₄[t1] ) by A12, A38, A53, A40, A45, A26; :: thesis:

end;

A54: 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 A55: sy in Terminals (DTConOSA X) ; :: thesis:
reconsider t1 = root-tree sy as Element of TS (DTConOSA X) by A55, DTCONSTR:def 1;
take t1 ; :: thesis:
thus t1 = root-tree sy ; :: thesis:
A56: (PTMin X) . (root-tree sy) = pi sy by A55, Def31
.= root-tree sy by A55, Def16 ;
hence (PTMin X) . t1 in OSClass ((PTCongruence X),t1) by Th32; :: thesis:
thus LeastSort ((PTMin X) . t1) <= LeastSort t1 by A56; :: thesis:
thus for s1 being Element of S
for x1 being set st x1 in X . s1 & t1 = root-tree [x1,s1] holds
(PTMin X) . t1 = t1 by A56; :: thesis:
A57: ex s being Element of S ex x being set st
( x in X . s & sy = [x,s] ) by A55, Th4;

hereby :: thesis:

let o be OperSymbol of S; :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
OSSym (o,X) ==> roots ts and
A58: t1 = (OSSym (o,X)) -tree ts ; :: thesis:
t1 . {} = [o, the carrier of S] by A58, TREES_4:def 4;
hence ( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym (o,X) ==> roots ((PTMin X) * ts) & OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) & (PTMin X) . t1 = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) ) by A57, Th10; :: thesis:

end;

for dt being DecoratedTree of the carrier of (DTConOSA X) st dt in TS (DTConOSA X) holds
S₅[dt] from DTCONSTR:sch 7(A54, A1);
then ex t1 being Element of TS (DTConOSA X) st
( t1 = t & S₁[t1] & S₂[t1] & S₃[t1] & S₄[t1] ) ;
hence ( (PTMin X) . t in OSClass ((PTCongruence X),t) & LeastSort ((PTMin X) . t) <= LeastSort t & ( for s being Element of S
for x being set st x in X . s & t = root-tree [x,s] holds
(PTMin X) . t = t ) & ( for o being OperSymbol of S
for ts being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots ts & t = (OSSym (o,X)) -tree ts holds
( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym (o,X) ==> roots ((PTMin X) * ts) & OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) & (PTMin X) . t = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) ) ) ) ; :: thesis: