I think you are missing some properties of successors (uniqueness and s(n) different than any m<= n)

That would avoid “branching” of two different successors to n and loops in which a successor is a smaller number than n