证明采用分类讨论（也称分情形讨论）：穷尽所有可能情形并逐一论证． 由于 $⟶$ 是最小关系，任何推导的最后一步只能出自那十条规则，因此只需按这十条规则分类即可穷尽所有情况，无需枚举无穷多个词项． 下面覆盖这十种情形，对称或重复的论证合并说明； 每个情形里，再按结论左边的形状排除不匹配的规则，检查第二个推导剩下的候选规则．

具体地，对 $𝑡⟶{𝑡}^{\prime }$ 作规则归纳（ 规则归纳法 ）， 要证的性质是“对任意 ${𝑡}^{″}$，$𝑡⟶{𝑡}^{″}$ 蕴涵 ${𝑡}^{\prime }={𝑡}^{″}$”． “任意 ${𝑡}^{″}$”必须写进性质里，否则 归纳假设 只能用于某个固定的 ${𝑡}^{″}$，在 E-If 情形就不够用． 每个情形里，再看 $𝑡⟶{𝑡}^{″}$ 的推导最后一步可能是哪条规则： 它的结论左边必须和 $𝑡$ 形状相同．

对 E-IfTrue，$𝑡=\text{ if }\text{ true }\text{ then }{𝑡}_2\text{ else }{𝑡}_3$，${𝑡}^{\prime }={𝑡}_2$． 第二个推导若是 E-IfTrue，则 ${𝑡}^{″}={𝑡}_2$； 条件为 $\text{true}$，排除了要求条件为 $\text{false}$ 的 E-IfFalse； 值不可规约 又排除了要求 $\text{true }⟶\dots$ 的 E-If． E-IfFalse 与上一条对称． 对 E-If，前提为 ${𝑡}_1⟶{𝑡}_1^{\prime }$；由于 ${𝑡}_1$ 能规约，由 值不可规约 知它不可能等于 $\text{true}$ 或 $\text{false}$，从而排除 E-IfTrue 与 E-IfFalse，第二个推导只能是 E-If（前提 ${𝑡}_1⟶{𝑡}_1^{″}$），由 归纳假设 得 ${𝑡}_1^{\prime }={𝑡}_1^{″}$，于是 ${𝑡}^{\prime }={𝑡}^{″}$．

对 E-Succ，左边形如 $\text{succ }\dots$ 的规则只有 E-Succ，由 归纳假设 即得． 对 E-PredZero，$𝑡=\text{ pred }0$；E-PredSucc 要求 $\text{pred}$ 后面是 $\text{succ }\dots$，不适用；E-Pred 要求 $0$ 能规约，与 值不可规约 矛盾，所以只能是 E-PredZero，${𝑡}^{″}=0={𝑡}^{\prime }$． 对 E-PredSucc， t = pred (succ nv)；E-PredZero 不适用，E-Pred 要求值 succ nv 能规约而矛盾，所以只能是 E-PredSucc，结果相同． 对 E-Pred，前提为 ${𝑡}_1⟶{𝑡}_1^{\prime }$；由 值不可规约 知 ${𝑡}_1$ 不属于值，而 E-PredZero 与 E-PredSucc 分别要求 ${𝑡}_1$ 为值 $0$ 或 succ nv，故都不适用，剩下 E-Pred，用 归纳假设 ． E-IsZeroZero、E-IsZeroSucc、E-IsZero 与 $\text{pred}$ 的三条一一对应，论证相同．