let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being non-empty 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 non-empty 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 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)
defpred S1[ set ] means ex t1 being Element of TS (DTConOSA X) st
( t1 = $1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) );
let t be Element of TS (DTConOSA X); :: thesis: [t,((PTMin X) . t)] in R . (LeastSort t)
A1: R is os-compatible by OSALG_4:def 2;
A2: 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
S1[dt1] ) holds
S1[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
S1[dt1] ) holds
S1[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
S1[dt1] ) implies S1[nt -tree ts1] )
assume that
A3: nt ==> roots ts1 and
A4: for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S1[dt1] ; :: thesis: S1[nt -tree ts1]
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 A3, Th12;
reconsider t1 = nt -tree ts1 as Element of TS (DTConOSA X) by A3, Th12;
A8: dom ((PTMin X) * ts1) = dom ts1 by FINSEQ_3:120;
reconsider tsa = ts1 as Element of Args (o,(ParsedTermsOSA X)) by A6;
set w = the_arity_of o;
A9: rng ts1 c= TS (DTConOSA X) by FINSEQ_1:def 4;
set lo = LBound (o,(LeastSorts ((PTMin X) * ts1)));
set rs1 = the_result_sort_of o;
A10: t1 = (OSSym (o,X)) -tree ts1 by A5;
then A11: OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),X) ==> roots ((PTMin X) * ts1) by A3, A5, Th40;
then reconsider tsm = (PTMin X) * ts1 as Element of Args ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X)) by Th13;
A12: dom ts1 = dom (the_arity_of o) by A6, MSUALG_3:6;
A13: 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 A14: y in dom tsm ; :: thesis: [(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y)
ts1 . y in rng ts1 by A8, A14, FUNCT_1:3;
then reconsider td1 = ts1 . y as Element of TS (DTConOSA X) by A9;
consider t2 being Element of TS (DTConOSA X) such that
A15: t2 = td1 and
A16: [t2,((PTMin X) . t2)] in R . (LeastSort t2) by A4, A8, A14, FUNCT_1:3;
A17: (PTMin X) . t2 = tsm . y by A14, A15, FINSEQ_3:120;
A18: (PTMin X) . t2 in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by A16, ZFMISC_1:87;
tsa . y in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. y) by A8, A12, A14, MSUALG_6:2;
then A19: LeastSort t2 <= (the_arity_of o) /. y by A15, Def12;
A20: t2 in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by A16, ZFMISC_1:87;
field (R . (LeastSort t2)) = the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by ORDERS_1:12;
then R . (LeastSort t2) is_symmetric_in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by RELAT_2:def 11;
then [((PTMin X) . t2),t2] in R . (LeastSort t2) by A16, A20, A18, RELAT_2:def 3;
hence [(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y) by A1, A15, A20, A18, A17, A19; :: thesis: verum
end;
LeastSorts ((PTMin X) * ts1) <= the_arity_of o by A3, A5, A10, Th40;
then LBound (o,(LeastSorts ((PTMin X) * ts1))) <= o by OSALG_1:35;
then A21: [((Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . tsm),((Den (o,(ParsedTermsOSA X))) . tsa)] in R . (the_result_sort_of o) by A13, OSALG_4:def 26;
then A22: (Den (o,(ParsedTermsOSA X))) . tsa in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by ZFMISC_1:87;
A23: LeastSort t1 = the_result_sort_of o by A6, A7, Th17;
A24: OSSym (o,X) ==> roots ts1 by A3, A5;
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)
field (R . (the_result_sort_of o)) = the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by ORDERS_1:12;
then A25: R . (the_result_sort_of o) is_symmetric_in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by RELAT_2:def 11;
(Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . tsm in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by A21, ZFMISC_1:87;
then A26: [((Den (o,(ParsedTermsOSA X))) . tsa),((Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . tsm)] in R . (the_result_sort_of o) by A21, A22, A25, RELAT_2:def 3;
consider o4 being OperSymbol of S such that
A27: OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),X) = [o4, the carrier of S] and
(PTMin X) * ts1 in Args (o4,(ParsedTermsOSA X)) and
A28: (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),X)) -tree ((PTMin X) * ts1) = (Den (o4,(ParsedTermsOSA X))) . ((PTMin X) * ts1) and
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 A11, Th12;
LBound (o,(LeastSorts ((PTMin X) * ts1))) = o4 by A27, XTUPLE_0:1;
hence [t1,((PTMin X) . t1)] in R . (LeastSort t1) by A5, A7, A24, A26, A23, A28, Th40; :: thesis: verum
end;
A29: for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S1[ root-tree s]
proof
let sy be Symbol of (DTConOSA X); :: thesis: ( sy in Terminals (DTConOSA X) implies S1[ root-tree sy] )
assume sy in Terminals (DTConOSA X) ; :: thesis: S1[ root-tree sy]
then A30: ex s being Element of S ex x being set st
( x in X . s & sy = [x,s] ) by Th4;
then reconsider t1 = root-tree sy as Element of TS (DTConOSA X) by Th10;
take t1 ; :: thesis: ( t1 = root-tree sy & [t1,((PTMin X) . t1)] in R . (LeastSort t1) )
A31: 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:12;
then A32: R . (LeastSort t1) is_reflexive_in the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by RELAT_2:def 9;
t1 = (PTMin X) . t1 by A30, Th40;
hence ( t1 = root-tree sy & [t1,((PTMin X) . t1)] in R . (LeastSort t1) ) by A31, A32, RELAT_2:def 1; :: thesis: verum
end;
for dt being DecoratedTree of the carrier of (DTConOSA X) st dt in TS (DTConOSA X) holds
S1[dt] from DTCONSTR:sch 7(A29, A2);
 then ex t1 being Element of TS (DTConOSA X) st
( t = t1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) ) ;
hence [t,((PTMin X) . t)] in R . (LeastSort t) ; :: thesis: verum