let S be OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: 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;
then reconsider nt1 = nt as NonTerminal of (DTConOSA X) by LANG1:def 3;
reconsider ts1 = ts as SubtreeSeq of nt1 by A1, DTCONSTR:def 6;
thus nt in NonTerminals (DTConOSA X) by A2, LANG1:def 3; :: thesis:
then nt in [: the carrier' of S,{ the carrier of S}:] by Th3;
then consider o1, b1 being object such that
A3: o1 in the carrier' of S and
A4: b1 in { the carrier of S} and
A5: nt = [o1,b1] by ZFMISC_1:def 2;
nt1 -tree ts1 in TS (DTConOSA X) ;
hence nt -tree ts in TS (DTConOSA X) ; :: thesis:
reconsider o1 = o1 as OperSymbol of S by A3;
take o1 ; :: thesis:
thus nt = [o1, the carrier of S] by A4, A5, TARSKI:def 1; :: thesis:
b1 = the carrier of S by A4, TARSKI:def 1;
then A6: (nt1 -tree ts) . {} = [o1, the carrier of S] by A5, TREES_4:def 4;
then ex p being SubtreeSeq of OSSym (o1,X) st
( 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;
hence ( 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 A6, Th11, TREES_4:15; :: thesis: