for t being DecoratedTree
for p being Node of t
for k being Element of NAT holds p | k is Node of t