一步规约 的 E-PredSucc 规则左边是 pred (succ nv)， 只允许 $\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$，所以这个项的最终结果没有变，但一步关系已不再确定． 仅凭这个例子还不能断言整个扩展语言的所有最终结果都不变，那需要另外的证明． 我们仍可以写一个按某种策略选后继的函数， 但它实现的是受策略限制后的关系，不能再声称它枚举了原关系的全部一步结果 （见 求值策略、规约策略与合流性 ）． 这个决定是由证明推动的：证明写不下去时，要么调整设计，要么调整所要保证的性质， 不能把缺口当作已经证明． 用测试对照证明 所述的确定性测试也抓到了放宽后的反例．