Research proof index

Reverse step correspondence: if p.toStandardForm steps from s to s', then either: (1) p steps from s to s' (same step), or (2) s' is halted in p.toStandardForm, and p steps to a state that is also halted with the same registers (this only happens for jumps with unbounded targets).

Forward step correspondence: if p steps from s to s', then either: (1) p.toStandardForm steps from s to s' (same step), or (2) s' is halted in p, and p.toStandardForm steps to a state that is also halted with the same registers (this only happens for jumps with unbounded targets).

If two halted states are reachable from the same start, they are equal. This follows from confluence: since Step p is confluent and both s₁ and s₂ are normal forms reachable from init, they must be equal.

Reverse halting: if p.toStandardForm reaches a halted state, p reaches a halted state with the same registers.

Forward halting: if p reaches a halted state, p.toStandardForm reaches a halted state with the same registers.

Straight-line programs halt from any starting registers, not just State.init. Useful for chaining: after running one program, we can run the next straight-line segment from whatever registers we're in.