按 [定义] 一步归约 的规则，取 $𝑡=\text{ succ }\left(\text{if }\text{ true }\text{ then }\text{ false }\text{ else }0\right)$。是否为值采用 [定义] 值与数值 ，是否受阻采用 [定义] 范式与受阻 。

第一步。$𝑡$ 的最外层是 $\text{succ}$。结论左边形如 $\text{succ }\dots$ 的规则只有 E-Succ，它要求里面的 $\text{if }\text{ true }\text{ then }\text{ false }\text{ else }0$ 能归约。这个 $\text{if}$ 的条件是 $\text{true}$，E-IfTrue 适用，得到 $\text{false}$。于是推导是：

第二步。现在的项是 $\text{succ }\text{ false}$。仍然只有 E-Succ 可能适用，它要求 $\text{false }⟶{𝑡}_{1^{\prime }}$ 对某个 ${𝑡}_{1^{\prime }}$ 成立。但 $\text{false}$ 是值，由 [引理] 值不可归约 不能归约，于是 E-Succ 的前提搭不上，没有任何规则可用：$\text{succ }\text{ false}$ 是范式。它又不是值（$\text{succ}$ 后面必须是数值），所以它受阻了。

第一步完全合法，问题出在第二步。所以一个项“现在还能归约”并不说明它“永远不会出错”。