for T being finite-branching DecoratedTree
for x, x9 being Element of dom T st x9 in succ x holds
T . x9 in rng (succ (T,x))