[定义] 一步归约 的 E-PredSucc 规则左边写的是 ，只允许 $\text{succ}$ 里面是 [定义] 值与数值 中的数值。看起来也可以放宽成任意项：

毕竟“先加一再减一”就是原来的数，何必等里面算完？问题在于，放宽以后同一个项会有两种归约方式。取 $𝑡=\text{ pred }\left(\text{succ }\left(\text{pred }0\right)\right)$：

• 用放宽后的规则，直接把外层的 $\text{pred }\left(\text{succ }\dots \right)$ 消掉：$𝑡⟶\text{ pred }0$；
• 用 E-Pred 和 E-Succ 两条同余规则往里找，在最里面用 E-PredZero：$𝑡⟶\text{ pred }\left(\text{succ }0\right)$。

两个结果不一样， [定理] 确定性 就不再成立。在证明里，这表现为 E-PredSucc 那个情形写不下去：要排除第二个推导是 E-Pred，需要“$\text{succ }𝑡$ 不能归约”，而 $𝑡$ 不一定是值，这一点推不出来。

这个例子里两条路最后都会到达 $0$，所以这个项的最终结果没有变，但一步关系已不再确定。仅凭这个例子还不能断言整个扩展语言的所有最终结果都不变，那需要另外的证明。我们仍可以写一个按某种策略选后继的函数，但它实现的是受策略限制后的关系，不能再声称它枚举了原关系的全部一步结果（见 [附注] 求值策略、归约策略与合流性 ）。这个决定是被证明逼出来的：证明写不下去时，要么调整设计，要么调整所要保证的性质，不能把缺口当作已经证明。 用测试对照证明 所述的确定性测试也抓到了放宽后的反例。