for t being finite-branching DecoratedTree ex x being set ex p being DTree-yielding FinSequence st t = x -tree p