CMP.12:5.4 - Preserve completion through internal steps

The source instruction is return 7; the receiving use requires that return. A target first takes k internal steps and then returns 7, where k is a supplied nonnegative integer. Use a remaining-step counter: each internal step reduces it by one, and at zero the target returns. For every finite k the counter proves that the internal phase finishes, so the target supplies the required result.

Change the target to loop: goto loop, leaving return 7 after this loop. Each internal step goes back to loop, so the return is unreachable. A correspondence that allows arbitrarily many silent steps without a completion argument would hide this failure. Restore a finite internal phase to meet the required return.