let S be OrderSortedSign; :: thesis:
let X be V16() 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 9;
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 set 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: