采用 [定义] 一步归约 的十条规则，${⟶}^{\ast }$ 表示 [定义] 多步归约 的零步或有限多步归约；终点是否为值按 [定义] 值与数值 判断。

$$\begin{array}{cc}& \text{ if }\left(\text{iszero }\left(\text{pred }\left(\text{succ }0\right)\right)\right)\text{ then }\text{ succ }0\text{ else }0\\ ⟶& \text{ if }\left(\text{iszero }0\right)\text{ then }\text{ succ }0\text{ else }0& & \text{ E-If + E-IsZero + E-PredSucc }\\ ⟶& \text{ if }\text{ true }\text{ then }\text{ succ }0\text{ else }0& & \text{ E-If + E-IsZeroZero }\\ ⟶& \text{ succ }0& & \text{ E-IfTrue}\end{array}$$

每行右边列出了这一步推导用到的规则，从外层的同余规则写到最里层的计算规则。三步之后到达值 $\text{succ }0$，所以

$$\text{if }\left(\text{iszero }\left(\text{pred }\left(\text{succ }0\right)\right)\right)\text{ then }\text{ succ }0\text{ else }0{⟶}^{\ast }\text{ succ }0$$

由 [定理] 确定性 ，每一步都别无选择，所以这条链是唯一的。${⟶}^{\ast }$ 也包括中间每一站：这个项也多步归约到第二行、第三行的项，以及它自己（零步）。