let S be OrderSortedSign; for X being V2() ManySortedSet of S
for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) ) )
let X be V2() ManySortedSet of S; for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) ) )
let nt be Symbol of (DTConOSA X); for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) ) )
let ts be FinSequence of TS (DTConOSA X); ( nt ==> roots ts implies ( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) ) ) )
assume A1:
nt ==> roots ts
; ( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) ) )
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; ( nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) ) )
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)
; ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(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 o <= s1 ) ) )
reconsider o1 = o1 as OperSymbol of S by A3;
take
o1
; ( nt = [o1, the carrier of S] & 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 ) ) )
thus
nt = [o1, the carrier of S]
by A4, A5, TARSKI:def 1; ( 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 ) ) )
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; verum