:: deftheorem Def6 defines succ TREES_9:def 6 :
for t being finite-branching DecoratedTree
for p being FinSequence st p in dom t holds
for b₃ being FinSequence holds
( b₃ = succ (t,p) iff ex q being Element of dom t st
( q = p & b₃ = t * (q succ) ) );