Research proof index

A program halts with result a iff evaluation returns Part.some a.

A state is halted iff it is normal (has no successor) in the reduction system.

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.