let S be monotone regular locally_directed OrderSortedSign; :: thesis:
let X be V5 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 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:
reconsider t1 = root-tree sy as Element of TS (DTConOSA X) by A2, DTCONSTR:def 4;
take t1 ; :: thesis:
thus t1 = root-tree sy ; :: thesis:
consider s being Element of S, x being set such that
A3: ( x in X . s & sy = [x,s] ) by A2, Th4;
let t2 be Element of TS (DTConOSA X); :: thesis:
assume A4: t2 in OSClass (PTCongruence X),t1 ; :: thesis:
thus (PTMin X) . t2 = (PTMin X) . t1 by A3, A4, Th34; :: thesis:

end;

A5: 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
A6: nt ==> roots ts1 and
A7: 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 A6, Th12;
take t1 ; :: thesis:
thus t1 = nt -tree ts1 ; :: thesis:
reconsider ta1 = t1 as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by Def12;
consider o being OperSymbol of S such that
A8: ( nt = [o,the carrier of S] & ts1 in Args o,(ParsedTermsOSA X) & nt -tree ts1 = (Den o,(ParsedTermsOSA X)) . ts1 & ( 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 A6, Th12;
A9: OSClass (PTCongruence X),t1 = OSClass (PTCongruence X),ta1 by Def28
.= proj1 ((PTClasses X) . t1) by Th26 ;
set Ms = (PTMin X) * ts1;
set w = the_arity_of o;
A10: ( dom ((PTClasses X) * ts1) = dom ts1 & dom ((PTMin X) * ts1) = dom ts1 & dom (LeastSorts ts1) = dom ts1 & dom ts1 = dom (the_arity_of o) ) by A8, Def14, ALG_1:1, MSUALG_3:6;
A11: rng ts1 c= TS (DTConOSA X) by FINSEQ_1:def 4;
( t1 = (OSSym o,X) -tree ts1 & OSSym o,X ==> roots ts1 ) by A6, A8;
then A12: ( (PTMin X) . t1 = (OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) & LeastSorts ((PTMin X) * ts1) <= the_arity_of o ) by Th41;
A13: (PTClasses X) . t1 = @ nt,((PTClasses X) * ts1) by A6, 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 ((PTClasses X) * ts1) & ( for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(x2 . y),(w3 /. y)] in ((PTClasses X) * ts1) . y ) ) ) } ;
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 A14: t3 in OSClass (PTCongruence X),t1 ; :: thesis:
consider s4 being set such that
A15: [t3,s4] in (PTClasses X) . t1 by A9, A14, RELAT_1:def 4;
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 A13, A15;
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 A8, A19, ZFMISC_1:33;
A21: ( x2 is FinSequence of TS (DTConOSA X) & OSSym o2,X ==> roots x2 ) by Th13;
reconsider ts3 = x2 as FinSequence of TS (DTConOSA X) by Th13;
( OSSym o2,X in NonTerminals (DTConOSA X) & (OSSym o2,X) -tree ts3 in TS (DTConOSA X) & 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 A21, Th12;
then consider o3 being OperSymbol of S such that
A22: ( OSSym o2,X = [o3,the carrier of S] & ts3 in Args o3,(ParsedTermsOSA X) & (OSSym o2,X) -tree ts3 = (Den o3,(ParsedTermsOSA X)) . ts3 ) ;
o2 = o3 by A22, ZFMISC_1:33;
then A23: t3 = (OSSym o2,X) -tree ts3 by A16, A22, ZFMISC_1:33;
A24: ( dom (the_arity_of o) = dom (the_arity_of o2) & dom ts3 = dom (the_arity_of o2) & dom ((PTMin X) * ts3) = dom ts3 ) by A19, A20, ALG_1:1, FINSEQ_3:31, MSUALG_3:6;
A25: 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

let k be Nat; :: thesis:
assume A26: k in dom ((PTMin X) * ts3) ; :: thesis:
A27: ( ts1 . k in rng ts1 & ts3 . k in rng ts3 ) by A10, A24, A26, FUNCT_1:12;
then reconsider tk1 = ts1 . k, tk3 = ts3 . k as Element of TS (DTConOSA X) by A11, A25;
consider tk2 being Element of TS (DTConOSA X) such that
A28: tk2 = tk1 and
A29: for t4 being Element of TS (DTConOSA X) st t4 in OSClass (PTCongruence X),tk2 holds
(PTMin X) . t4 = (PTMin X) . tk2 by A7, A27;
reconsider tak = tk1 as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort tk1) by Def12;
A30: OSClass (PTCongruence X),tk1 = OSClass (PTCongruence X),tak by Def28
.= proj1 ((PTClasses X) . tk1) by Th26 ;
consider w3 being Element of the carrier of S * such that
dom w3 = dom ((PTClasses X) * ts1) and
A31: for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(x2 . y),(w3 /. y)] in ((PTClasses X) * ts1) . y by A18;
[tk3,(w3 /. k)] in ((PTClasses X) * ts1) . k by A10, A24, A26, A31;
then [tk3,(w3 /. k)] in (PTClasses X) . tk1 by A10, A24, A26, ALG_1:1;
then tk3 in proj1 ((PTClasses X) . tk1) by FUNCT_5:4;
then (PTMin X) . tk3 = (PTMin X) . tk1 by A28, A29, A30;
then (PTMin X) . tk3 = ((PTMin X) * ts1) . k by A10, A24, A26, ALG_1:1;
hence ((PTMin X) * ts3) . k = ((PTMin X) * ts1) . k by A26, ALG_1:1; :: thesis:

end;

then A32: (PTMin X) * ts3 = (PTMin X) * ts1 by A10, A24, FINSEQ_1:17;
( (PTMin X) . t3 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts3))),X) -tree ((PTMin X) * ts3) & LeastSorts ((PTMin X) * ts3) <= the_arity_of o2 ) by A21, A23, Th41;
hence (PTMin X) . t3 = (PTMin X) . t1 by A12, A19, A20, A32, OSALG_1:34; :: 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(A1, A5);
then consider t1 being Element of TS (DTConOSA X) such that
A33: ( t1 = t & S₁[t1] ) ;
thus S₁[t] by A33; :: thesis: