按 一步规约 的规则， 取 $𝑡=\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}$ 后面必须是数值，$\text{succ }\text{ false}$ 不属于值，因此受阻了．

第一步完全合法，问题出在第二步：词项当前能规约，并不保证后续步步都能正常推进．