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 nt in { s where s is Symbol of G : ex rts being FinSequence st s ==> rts } ;
hence nt is NonTerminal of G by LANG1:def 3; :: thesis:
consider rtl, rtr being Symbol of G such that
A2: roots ts = <*rtl,rtr*> by A1, Def4;
A3: ( dom <*rtl,rtr*> = dom ts & ( for i being Element of NAT st i in dom ts holds
ex T being DecoratedTree st
( T = ts . i & <*rtl,rtr*> . i = T . {} ) ) ) by A2, TREES_3:def 18;
A4: len <*rtl,rtr*> = 2 by FINSEQ_1:61;
hence dom ts = {1,2} by A3, FINSEQ_1:4, 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 & <*rtl,rtr*> . 1 = tl . {} ) by A2, TREES_3:def 18;
consider tr being DecoratedTree such that
A7: ( tr = ts . 2 & <*rtl,rtr*> . 2 = tr . {} ) by A2, A5, TREES_3:def 18;
( rng ts c= TS G & tl in rng ts & tr in rng ts ) by A5, A6, A7, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider tl = tl, tr = tr as Element of TS G ;
A8: ( <*rtl,rtr*> . 1 = rtl & <*rtl,rtr*> . 2 = rtr ) by FINSEQ_1:61;
Seg (len <*rtl,rtr*>) = dom <*rtl,rtr*> by FINSEQ_1:def 3
.= Seg (len ts) by A3, FINSEQ_1:def 3 ;
then len ts = 2 by A4, FINSEQ_1:8;
then A9: ts = <*tl,tr*> by A6, A7, FINSEQ_1:61;
take tl ; :: thesis:
take tr ; :: thesis:
thus roots ts = <*(root-label tl),(root-label tr)*> by A2, A6, A7, A8; :: thesis:
thus ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree tl,tr ) by A6, A7, A9, TREES_4:def 6; :: thesis:
thus ( tl in rng ts & tr in rng ts ) by A5, A6, A7, FUNCT_1:def 5; :: thesis: