let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V5 ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
let X be V5 ManySortedSet of S; :: thesis: for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set F = PTClasses X;
set M = PTMin X;
let R be MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X; :: thesis: for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
A1: R is os-compatible by OSALG_4:def 3;
defpred S₁[ set ] means ex t1 being Element of TS (DTConOSA X) st
( t1 = $1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) );
A2: 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: ( sy in Terminals (DTConOSA X) implies S₁[ root-tree sy] )
assume A3: sy in Terminals (DTConOSA X) ; :: thesis: S₁[ root-tree sy]
consider s being Element of S, x being set such that
A4: ( x in X . s & sy = [x,s] ) by A3, Th4;
reconsider t1 = root-tree sy as Element of TS (DTConOSA X) by A4, Th10;
take t1 ; :: thesis: ( t1 = root-tree sy & [t1,((PTMin X) . t1)] in R . (LeastSort t1) )
A5: t1 = (PTMin X) . t1 by A4, Th41;
A6: t1 in the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by Def12;
field (R . (LeastSort t1)) = the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by ORDERS_1:97;
then R . (LeastSort t1) is_reflexive_in the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by RELAT_2:def 9;
hence ( t1 = root-tree sy & [t1,((PTMin X) . t1)] in R . (LeastSort t1) ) by A5, A6, RELAT_2:def 1; :: thesis: verum

end;

A7: 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: 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]
let ts1 be FinSequence of TS (DTConOSA X); :: thesis: ( nt ==> roots ts1 & ( for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S₁[dt1] ) implies S₁[nt -tree ts1] )
assume that
A8: nt ==> roots ts1 and
A9: for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S₁[dt1] ; :: thesis: S₁[nt -tree ts1]
reconsider t1 = nt -tree ts1 as Element of TS (DTConOSA X) by A8, Th12;
take t1 ; :: thesis: ( t1 = nt -tree ts1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) )
thus t1 = nt -tree ts1 ; :: thesis: [t1,((PTMin X) . t1)] in R . (LeastSort t1)
consider o being OperSymbol of S such that
A10: ( 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 A8, Th12;
set w = the_arity_of o;
A11: ( 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 A10, Def14, ALG_1:1, MSUALG_3:6;
A12: rng ts1 c= TS (DTConOSA X) by FINSEQ_1:def 4;
A13: ( OSSym o,X ==> roots ts1 & t1 = (OSSym o,X) -tree ts1 ) by A8, A10;
then A14: ( LeastSort ((PTMin X) . t1) <= LeastSort t1 & LeastSorts ((PTMin X) * ts1) <= the_arity_of o & OSSym o,X ==> roots ((PTMin X) * ts1) & OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X ==> roots ((PTMin X) * ts1) & (PTMin X) . t1 = (OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) ) by Th41;
set lo = LBound o,(LeastSorts ((PTMin X) * ts1));
set rs1 = the_result_sort_of o;
A15: LBound o,(LeastSorts ((PTMin X) * ts1)) <= o by A14, OSALG_1:35;
reconsider tsa = ts1 as Element of Args o,(ParsedTermsOSA X) by A10;
reconsider tsm = (PTMin X) * ts1 as Element of Args (LBound o,(LeastSorts ((PTMin X) * ts1))),(ParsedTermsOSA X) by A14, Th13;
for y being Nat st y in dom tsm holds
[(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y)

proof

let y be Nat; :: thesis: ( y in dom tsm implies [(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y) )
assume A16: y in dom tsm ; :: thesis: [(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y)
A17: ts1 . y in rng ts1 by A11, A16, FUNCT_1:12;
then reconsider td1 = ts1 . y as Element of TS (DTConOSA X) by A12;
consider t2 being Element of TS (DTConOSA X) such that
A18: t2 = td1 and
A19: [t2,((PTMin X) . t2)] in R . (LeastSort t2) by A9, A17;
A20: ( t2 in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) & (PTMin X) . t2 in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) ) by A19, ZFMISC_1:106;
field (R . (LeastSort t2)) = the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by ORDERS_1:97;
then R . (LeastSort t2) is_symmetric_in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by RELAT_2:def 11;
then A21: [((PTMin X) . t2),t2] in R . (LeastSort t2) by A19, A20, RELAT_2:def 3;
A22: (PTMin X) . t2 = tsm . y by A16, A18, ALG_1:1;
tsa . y in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. y) by A11, A16, MSUALG_6:2;
then LeastSort t2 <= (the_arity_of o) /. y by A18, Def12;
hence [(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y) by A1, A18, A20, A21, A22, OSALG_4:def 1; :: thesis: verum

end;

then A23: [((Den (LBound o,(LeastSorts ((PTMin X) * ts1))),(ParsedTermsOSA X)) . tsm),((Den o,(ParsedTermsOSA X)) . tsa)] in R . (the_result_sort_of o) by A15, OSALG_4:def 28;
then A24: ( (Den (LBound o,(LeastSorts ((PTMin X) * ts1))),(ParsedTermsOSA X)) . tsm in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) & (Den o,(ParsedTermsOSA X)) . tsa in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) ) by ZFMISC_1:106;
field (R . (the_result_sort_of o)) = the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by ORDERS_1:97;
then R . (the_result_sort_of o) is_symmetric_in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by RELAT_2:def 11;
then A25: [((Den o,(ParsedTermsOSA X)) . tsa),((Den (LBound o,(LeastSorts ((PTMin X) * ts1))),(ParsedTermsOSA X)) . tsm)] in R . (the_result_sort_of o) by A23, A24, RELAT_2:def 3;
A26: LeastSort t1 = the_result_sort_of o by A10, Th18;
consider o4 being OperSymbol of S such that
A27: ( OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X = [o4,the carrier of S] & (PTMin X) * ts1 in Args o4,(ParsedTermsOSA X) & (OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) = (Den o4,(ParsedTermsOSA X)) . ((PTMin X) * ts1) & ( for s1 being Element of S holds
( (OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o4 <= s1 ) ) ) by A14, Th12;
LBound o,(LeastSorts ((PTMin X) * ts1)) = o4 by A27, ZFMISC_1:33;
hence [t1,((PTMin X) . t1)] in R . (LeastSort t1) by A10, A13, A25, A26, A27, Th41; :: thesis: verum

end;

A28: for dt being DecoratedTree of the carrier of (DTConOSA X) st dt in TS (DTConOSA X) holds
S₁[dt] from DTCONSTR:sch 7(A2, A7);
let t be Element of TS (DTConOSA X); :: thesis: [t,((PTMin X) . t)] in R . (LeastSort t)
consider t1 being Element of TS (DTConOSA X) such that
A29: ( t = t1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) ) by A28;
thus [t,((PTMin X) . t)] in R . (LeastSort t) by A29; :: thesis: verum