let S be OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: thesis:
let nt be Symbol of (DTConOSA X); :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume A1: nt ==> roots ts ; :: thesis:
set D = DTConOSA X;
set PTA = ParsedTermsOSA X;
A2: nt in { s where s is Symbol of (DTConOSA X) : ex n being FinSequence st s ==> n } by A1;
hence nt in NonTerminals (DTConOSA X) by LANG1:def 3; :: thesis:
then nt in [:the carrier' of S,{the carrier of S}:] by Th3;
then consider o1, b1 being set such that
A3: ( o1 in the carrier' of S & b1 in {the carrier of S} & nt = [o1,b1] ) by ZFMISC_1:def 2;
reconsider o1 = o1 as OperSymbol of S by A3;
reconsider nt1 = nt as NonTerminal of (DTConOSA X) by A2, LANG1:def 3;
reconsider ts1 = ts as SubtreeSeq of nt1 by A1, DTCONSTR:def 9;
nt1 -tree ts1 in TS (DTConOSA X) ;
hence nt -tree ts in TS (DTConOSA X) ; :: thesis:
A4: b1 = the carrier of S by A3, TARSKI:def 1;
take o1 ; :: thesis:
thus nt = [o1,the carrier of S] by A3, TARSKI:def 1; :: thesis:
A5: (nt1 -tree ts) . {} = [o1,the carrier of S] by A3, A4, TREES_4:def 4;
then consider p being SubtreeSeq of OSSym o1,X such that
A6: ( nt1 -tree ts1 = (OSSym o1,X) -tree p & OSSym o1,X ==> roots p & p in Args o1,(ParsedTermsOSA X) & nt1 -tree ts1 = (Den o1,(ParsedTermsOSA X)) . p ) by Th11;
thus ( ts in Args o1,(ParsedTermsOSA X) & nt -tree ts = (Den o1,(ParsedTermsOSA X)) . ts & ( for s1 being Element of S holds
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o1 <= s1 ) ) ) by A5, A6, Th11, TREES_4:15; :: thesis: