Rust 求值器 step step 用模式匹配实现 一步规约 的规则． match match 按书写顺序尝试分支； 要说明这种优先级没有漏掉合法后继，不能只说“函数每次返回一个结果”．

确定性 保证的是后继唯一，需要注意它与适用的规则唯一并不完全等同． 例如另加一条名字不同、结论也为 $\text{pred }0⟶0$ 的规则， 两条规则就同时适用，却产生相同的后继．

对于原来的十条规则，互斥性要靠具体排除论证： 条件是 $\text{true}$ 或 $\text{false}$ 时，由 值不可规约 ，E-If 的前提不成立； $\text{pred}$ 的参数是 $0$ 或 succ nv 时，参数也是值， E-Pred 的前提不成立，两个计算形状又彼此不同； $\text{iszero}$ 的情形相同． 参数能规约时，反过来排除这些计算形状． 这些正是确定性证明中用到的逐形状分析．

因此，代码先列计算分支、再列递归分支，不会把另一条适用的规则藏起来． 分支内部是否返回了正确的项，还要由 求值器与一步规约一致 的双向对应保证． 若放宽 E-PredSucc 的数值限制，排除论证就失效，单后继函数只能另外选择策略， 见 E-PredSucc 的数值限制 ．