for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (T * (t succ)) = dom (t succ)