let G be non empty with_terminals with_nonterminals binary DTConstrStr ; :: thesis:
let ts be FinSequence of TS G; :: thesis:
let nt be Symbol of G; :: thesis:
assume A1: nt ==> roots ts ; :: thesis:
then consider rtl, rtr being Symbol of G such that
A2: roots ts = <*rtl,rtr*> by Def4;
nt in { s where s is Symbol of G : ex rts being FinSequence st s ==> rts } by A1;
hence nt is NonTerminal of G by LANG1:def 3; :: thesis:
A3: len <*rtl,rtr*> = 2 by FINSEQ_1:44;
A4: dom <*rtl,rtr*> = dom ts by A2, TREES_3:def 18;
hence dom ts = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def 3; :: thesis:
hence A5: ( 1 in dom ts & 2 in dom ts ) by TARSKI:def 2; :: thesis:
then consider tl being DecoratedTree such that
A6: tl = ts . 1 and
A7: <*rtl,rtr*> . 1 = tl . {} by A2, TREES_3:def 18;
A8: ( rng ts c= TS G & tl in rng ts ) by A5, A6, FINSEQ_1:def 4, FUNCT_1:def 3;
consider tr being DecoratedTree such that
A9: tr = ts . 2 and
A10: <*rtl,rtr*> . 2 = tr . {} by A2, A5, TREES_3:def 18;
tr in rng ts by A5, A9, FUNCT_1:def 3;
then reconsider tl = tl, tr = tr as Element of TS G by A8;
take tl ; :: thesis:
take tr ; :: thesis:
thus roots ts = <*(root-label tl),(root-label tr)*> by A2, A7, A10; :: thesis:
Seg (len <*rtl,rtr*>) = dom <*rtl,rtr*> by FINSEQ_1:def 3
.= Seg (len ts) by A4, FINSEQ_1:def 3 ;
then len ts = 2 by A3, FINSEQ_1:6;
then ts = <*tl,tr*> by A6, A9, FINSEQ_1:44;
hence ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) ) by TREES_4:def 6; :: thesis:
thus ( tl in rng ts & tr in rng ts ) by A5, A6, A9, FUNCT_1:def 3; :: thesis: