:: deftheorem Def12 defines PreTraversal DTCONSTR:def 12 :
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 the carrier of G holds
( b₃ = PreTraversal tsg iff ex f being Function of (TS G),( the carrier of 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
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) );