• $\text{succ }\left(\text{succ }0\right)$ 是数值，也是值和范式，不受阻。
• $\text{pred }\left(\text{succ }0\right)$ 不是值，也不是范式：E-PredSucc 给出后继 $0$，所以现在不受阻。
• $\text{succ }\text{ true}$ 不是值，是受阻的范式：唯一候选 E-Succ 的前提无法成立。
• $\text{if }\text{ true }\text{ then }0\text{ else }\left(\text{succ }\text{ true}\right)$ 不是值，也不是范式；E-IfTrue 直接给出 $0$。未选中的坏分支不参与求值。
• $\text{if }0\text{ then }0\text{ else }0$ 不是值，是受阻的范式：条件不是布尔值，也不能归约。

因此“不是值”不等于“受阻”，“有坏的子项”也不等于“现在受阻”。

$$\begin{array}{cc}& \text{ pred }\left(\text{if }\left(\text{iszero }\left(\text{pred }0\right)\right)\text{ then }\text{ succ }\left(\text{succ }0\right)\text{ else }0\right)\\ ⟶& \text{ pred }\left(\text{if }\left(\text{iszero }0\right)\text{ then }\text{ succ }\left(\text{succ }0\right)\text{ else }0\right)\\ ⟶& \text{ pred }\left(\text{if }\text{ true }\text{ then }\text{ succ }\left(\text{succ }0\right)\text{ else }0\right)\\ ⟶& \text{ pred }\left(\text{succ }\left(\text{succ }0\right)\right)\\ ⟶& \text{ succ }0\end{array}$$

四步所用的规则依次是 E-Pred + E-If + E-IsZero + E-PredZero，E-Pred + E-If + E-IsZeroZero，E-Pred + E-IfTrue，E-PredSucc。第一步的完整推导是：

最后 $\text{succ }0$ 是值，没有后继。多步归约还包括链的中间各站与起点自身，不只是最终结果。

把 E-PredSucc 改成允许任意 $𝑡$ 的 $\text{pred }\left(\text{succ }𝑡\right)⟶𝑡$ 后，取 $𝑠=\text{ pred }\left(\text{succ }\left(\text{iszero }0\right)\right)$。直接消去外层得到 $𝑠⟶\text{ iszero }0$；先用同余规则进入内部，得到 $𝑠⟶\text{ pred }\left(\text{succ }\text{ true}\right)$。

两个后继不同，所以一步关系不确定。第一条路线再用 E-IsZeroZero 到 $\text{true}$，第二条路线再用放宽的 E-PredSucc 到 $\text{true}$；因此这个分叉可以汇合。但一个可汇合的例子不证明整套扩展关系合流。

Rust 函数即使按分支优先级选出唯一返回值，也没有消除关系的另一条合法路线。要么实现“所有后继”的接口，要么明确说这个单后继函数实现的是选定策略限制后的关系。注意扩展规则下 $\text{pred }\left(\text{succ }\text{ true}\right)$ 能归约，不能照搬它在原语言中受阻的判断。

"" == 0 "" == 0 和 0 == "0" 0 == "0" 为 true true ， "" == "0" "" == "0" 为 false false ；三组 === === 都为 false false 。前两次把字符串转为数字，第三次只比较两个不同的字符串。

使用 [附注] 相等关系的“地狱”给语言设计什么教训 的自定义 == == 去重算法，输入 ["", 0, "0"] ["", 0, "0"] 留下 ["", "0"] ["", "0"] ，输入 [0, "", "0"] [0, "", "0"] 只留下 [0] [0] 。规则明确仍可能失去算法所依赖的传递性；改用 === === 后这三种输入彼此不同，不会在这个例子中被合并，但仍要留意对象身份和 NaN NaN 的特殊处理。

对 $\text{if }\text{ true }\text{ then }0\text{ else }\left(\text{succ }\text{ true}\right)$，原语言与错误扩展都用 E-IfTrue 直接得到 $0$，不计算 else 分支。

原语言中的 $\text{pred }\left(\text{succ }\text{ false}\right)$ 没有后继，是受阻的范式。错误扩展先在内部用 E-OpBool，并由 E-Pred 提升到整项，得到 $\text{pred }\text{ wrong}$；再用 E-OpWrong 到 $\text{wrong}$。它是明确的异常终点，不是普通数值。

$\text{wrong}$ 是错误项， IllegalArgumentException IllegalArgumentException 是异常对象，$\perp$ 是底类型。Kotlin 的抛异常表达式可以具有 Nothing Nothing 类型，不意味着异常对象是底类型的值，也不意味着未选中的异常分支必须先执行。