let G be non empty with_terminals with_nonterminals binary DTConstrStr ; for ts being FinSequence of TS G
for nt being Symbol of G st nt ==> roots ts holds
( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )
let ts be FinSequence of TS G; for nt being Symbol of G st nt ==> roots ts holds
( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )
let nt be Symbol of G; ( nt ==> roots ts implies ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) )
assume A1:
nt ==> roots ts
; ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )
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; ( dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )
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; ( 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )
hence A5:
( 1 in dom ts & 2 in dom ts )
by TARSKI:def 2; ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )
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
; ex tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )
take
tr
; ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )
<*rtl,rtr*> . 1 = rtl
by FINSEQ_1:44;
hence
roots ts = <*(root-label tl),(root-label tr)*>
by A2, A7, A10, FINSEQ_1:44; ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )
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 A6, A9, TREES_4:def 6; ( tl in rng ts & tr in rng ts )
thus
( tl in rng ts & tr in rng ts )
by A5, A6, A9, FUNCT_1:def 3; verum