let S be monotone regular locally_directed OrderSortedSign; :: thesis:
let X be V2() 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 for t1 being Element of TS (DTConOSA X) st t1 in OSClass ((PTCongruence X),$1) holds
(PTMin X) . t1 = (PTMin X) . $1;
defpred S₂[ DecoratedTree of the carrier of (DTConOSA X)] means ex t1 being Element of TS (DTConOSA X) st
( t1 = $1 & 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] ) ; :: thesis:
reconsider t1 = nt -tree ts1 as Element of TS (DTConOSA X) by A2, Th12;
A4: (PTClasses X) . t1 = @ (nt,((PTClasses X) * ts1)) 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 ((PTClasses X) * ts1) & ( for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(x2 . y),(w3 /. y)] in ((PTClasses X) * ts1) . y ) ) ) } ;
consider o being OperSymbol of S such that
A5: nt = [o, the carrier of S] and
A6: ts1 in Args (o,(ParsedTermsOSA X)) and
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;
A7: t1 = (OSSym (o,X)) -tree ts1 by A5;
then A8: LeastSorts ((PTMin X) * ts1) <= the_arity_of o by A2, A5, Th40;
set Ms = (PTMin X) * ts1;
set w = the_arity_of o;
A9: dom ts1 = dom (the_arity_of o) by A6, MSUALG_3:6;
reconsider ta1 = t1 as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by Def12;
take t1 ; :: thesis:
thus t1 = nt -tree ts1 ; :: thesis:
A10: dom ((PTClasses X) * ts1) = dom ts1 by FINSEQ_3:120;
A11: OSClass ((PTCongruence X),t1) = OSClass ((PTCongruence X),ta1) by Def27
.= proj1 ((PTClasses X) . t1) by Th25 ;
A12: rng ts1 c= TS (DTConOSA X) by FINSEQ_1:def 4;
A13: dom ((PTMin X) * ts1) = dom ts1 by FINSEQ_3:120;
A14: (PTMin X) . t1 = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),X)) -tree ((PTMin X) * ts1) by A2, A5, A7, Th40;
thus for t3 being Element of TS (DTConOSA X) st t3 in OSClass ((PTCongruence X),t1) holds
(PTMin X) . t3 = (PTMin X) . t1 :: thesis:

proof

let t3 be Element of TS (DTConOSA X); :: thesis:
assume t3 in OSClass ((PTCongruence X),t1) ; :: thesis:
then consider s4 being object such that
A15: [t3,s4] in (PTClasses X) . t1 by A11, XTUPLE_0:def 12;
consider o2 being OperSymbol of S, x2 being Element of Args (o2,(ParsedTermsOSA X)), s3 being Element of S such that
A16: [t3,s4] = [((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 ) and
A18: ex w3 being Element of the carrier of S * st
( dom w3 = dom ((PTClasses X) * ts1) & ( for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(x2 . y),(w3 /. y)] in ((PTClasses X) * ts1) . y ) ) by A4, A15;
consider o1 being OperSymbol of S such that
A19: nt = [o1, the carrier of S] and
A20: o1 ~= o2 and
A21: 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 A17;
A22: o1 = o by A5, A19, XTUPLE_0:1;
then A23: dom (the_arity_of o) = dom (the_arity_of o2) by A21, FINSEQ_3:29;
reconsider ts3 = x2 as FinSequence of TS (DTConOSA X) by Th13;
A24: dom ts3 = dom (the_arity_of o2) by MSUALG_3:6;
A25: dom ((PTMin X) * ts3) = dom ts3 by FINSEQ_3:120;
A26: rng ts3 c= TS (DTConOSA X) by FINSEQ_1:def 4;
for k being Nat st k in dom ((PTMin X) * ts3) holds
((PTMin X) * ts3) . k = ((PTMin X) * ts1) . k

proof

consider w3 being Element of the carrier of S * such that
dom w3 = dom ((PTClasses X) * ts1) and
A27: for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(x2 . y),(w3 /. y)] in ((PTClasses X) * ts1) . y by A18;
let k be Nat; :: thesis:
assume A28: k in dom ((PTMin X) * ts3) ; :: thesis:
A29: ts3 . k in rng ts3 by A25, A28, FUNCT_1:3;
ts1 . k in rng ts1 by A9, A23, A24, A25, A28, FUNCT_1:3;
then reconsider tk1 = ts1 . k, tk3 = ts3 . k as Element of TS (DTConOSA X) by A12, A26, A29;
reconsider tak = tk1 as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort tk1) by Def12;
consider tk2 being Element of TS (DTConOSA X) such that
A30: tk2 = tk1 and
A31: for t4 being Element of TS (DTConOSA X) st t4 in OSClass ((PTCongruence X),tk2) holds
(PTMin X) . t4 = (PTMin X) . tk2 by A3, A9, A23, A24, A25, A28, FUNCT_1:3;
[tk3,(w3 /. k)] in ((PTClasses X) * ts1) . k by A10, A9, A23, A24, A25, A28, A27;
then A32: [tk3,(w3 /. k)] in (PTClasses X) . tk1 by A10, A9, A23, A24, A25, A28, FINSEQ_3:120;
OSClass ((PTCongruence X),tk1) = OSClass ((PTCongruence X),tak) by Def27
.= proj1 ((PTClasses X) . tk1) by Th25 ;
then tk3 in OSClass ((PTCongruence X),tk1) by A32, XTUPLE_0:def 12;
then (PTMin X) . tk3 = (PTMin X) . tk1 by A30, A31;
then (PTMin X) . tk3 = ((PTMin X) * ts1) . k by A13, A9, A23, A24, A25, A28, FINSEQ_3:120;
hence ((PTMin X) * ts3) . k = ((PTMin X) * ts1) . k by A28, FINSEQ_3:120; :: thesis:

end;

then A33: (PTMin X) * ts3 = (PTMin X) * ts1 by A13, A9, A23, A25, FINSEQ_1:13, MSUALG_3:6;
A34: OSSym (o2,X) ==> roots x2 by Th13;
then ex o3 being OperSymbol of S st
( OSSym (o2,X) = [o3, the carrier of S] & ts3 in Args (o3,(ParsedTermsOSA X)) & (OSSym (o2,X)) -tree ts3 = (Den (o3,(ParsedTermsOSA X))) . ts3 & ( for s1 being Element of S holds
( (OSSym (o2,X)) -tree ts3 in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o3 <= s1 ) ) ) by Th12;
then consider o3 being OperSymbol of S such that
A35: OSSym (o2,X) = [o3, the carrier of S] and
ts3 in Args (o3,(ParsedTermsOSA X)) and
A36: (OSSym (o2,X)) -tree ts3 = (Den (o3,(ParsedTermsOSA X))) . ts3 ;
o2 = o3 by A35, XTUPLE_0:1;
then A37: t3 = (OSSym (o2,X)) -tree ts3 by A16, A36, XTUPLE_0:1;
then A38: LeastSorts ((PTMin X) * ts3) <= the_arity_of o2 by A34, Th40;
(PTMin X) . t3 = (OSSym ((LBound (o2,(LeastSorts ((PTMin X) * ts3)))),X)) -tree ((PTMin X) * ts3) by A34, A37, Th40;
hence (PTMin X) . t3 = (PTMin X) . t1 by A14, A8, A20, A22, A33, A38, OSALG_1:34; :: thesis:

end;

A39: 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 A40: sy in Terminals (DTConOSA X) ; :: thesis:
reconsider t1 = root-tree sy as Element of TS (DTConOSA X) by A40, DTCONSTR:def 1;
take t1 ; :: thesis:
thus t1 = root-tree sy ; :: thesis:
A41: ex s being Element of S ex x being set st
( x in X . s & sy = [x,s] ) by A40, Th4;
let t2 be Element of TS (DTConOSA X); :: thesis:
assume t2 in OSClass ((PTCongruence X),t1) ; :: thesis:
hence (PTMin X) . t2 = (PTMin X) . t1 by A41, Th33; :: 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(A39, A1);
then ex t1 being Element of TS (DTConOSA X) st
( t1 = t & S₁[t1] ) ;
hence for t1 being Element of TS (DTConOSA X) st t1 in OSClass ((PTCongruence X),t) holds
(PTMin X) . t1 = (PTMin X) . t ; :: thesis: