:: deftheorem Def11 defines TerminalString DTCONSTR:def 11 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b₃ being FinSequence of Terminals G holds
( b₃ = TerminalString tsg iff ex f being Function of (TS G),((Terminals G) *) st
( b₃ = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) );