证明的方法是穷举（case analysis，也叫分情形讨论）：把所有可能的情形一个不漏地列出来，逐个证明。穷举法成立的前提是情形确实覆盖了每一种可能，漏掉一种，整个证明就不成立。这里能保证不漏，是因为 $⟶$ 是最小关系，任何推导的最后一步只能是十条规则之一，所以下面恰好列十种情形；而在每种情形内部，又要对第二个推导的最后一步再穷举一次十条规则，逐条说明“适用”或“为什么不适用”。

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

• E-IfTrue：$𝑡=\text{ if }\text{ true }\text{ then }{𝑡}_2\text{ else }{𝑡}_3$，${𝑡}^{\prime }={𝑡}_2$。第二个推导若是 E-IfTrue，${𝑡}^{″}={𝑡}_2$。不可能是 E-IfFalse，条件不是 $\text{false}$。不可能是 E-If，那需要 $\text{true }⟶\dots$，与 [引理] 值不可归约 矛盾。
• E-IfFalse：与上一条对称。
• E-If：前提 ${𝑡}_1⟶{𝑡}_{1^{\prime }}$。第二个推导不可能是 E-IfTrue 或 E-IfFalse：那时 ${𝑡}_1$ 是 $\text{true}$ 或 $\text{false}$，而 ${𝑡}_1$ 能归约，与 [引理] 值不可归约 矛盾。所以它是 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：。E-PredZero 不适用；E-Pred 要求 能归约，但它是值，矛盾。所以只能是 E-PredSucc，结果相同。
• E-Pred：前提 ${𝑡}_1⟶{𝑡}_{1^{\prime }}$，所以 ${𝑡}_1$ 不是值（ [引理] 值不可归约 ），E-PredZero 和 E-PredSucc 都不适用（它们要求 ${𝑡}_1$ 是 $0$ 或 ，都是值）。剩下 E-Pred，用 归纳假设 。
• E-IsZeroZero、E-IsZeroSucc、E-IsZero：与 $\text{pred}$ 的三条一一对应，论证相同。