for t being finite DecoratedTree
for p being Element of dom t holds
( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) )