采用 一步规约 的十条规则， ${⟶}^{\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 }$ 也包括中间每一站：这个项也多步规约到第二行、第三行的项，以及它自己（零步）．