对 $𝑡⟶{𝑡}^{\prime }$ 作规则归纳（ [定理] 规则归纳法（rule induction） ），按最后一步的规则分情形。

• E-IfTrue、E-IfFalse：整项的大小是 $1+\mathrm{size}\left({𝑡}_1\right)+\mathrm{size}\left({𝑡}_2\right)+\mathrm{size}\left({𝑡}_3\right)$，结果只是被选中的一个分支，严格更小。
• E-PredZero、E-IsZeroZero：$\mathrm{size}\left(\text{pred }0\right)=\mathrm{size}\left(\text{iszero }0\right)=2$，结果 $0$ 或 $\text{true}$ 的大小为 $1$。
• E-PredSucc： size(pred (succ nv)) = size(nv) + 2，结果是 nv。
• E-IsZeroSucc： size(iszero (succ nv)) = size(nv) + 2 ≥ 3，结果 $\text{false}$ 的大小为 $1$。
• E-Succ、E-Pred、E-IsZero：前提 ${𝑡}_1⟶{𝑡}_1^{\prime }$，由 归纳假设 $\mathrm{size}\left({𝑡}_1^{\prime }\right)<\mathrm{size}\left({𝑡}_1\right)$。两边都只多包一层同一个一元节点，严格不等式仍成立。
• E-If：前提 ${𝑡}_1⟶{𝑡}_1^{\prime }$，由 归纳假设 条件部分变小，另两个分支与根节点不变，整项严格变小。

对步数：设 $𝑡={𝑡}_0⟶{𝑡}_1⟶\cdots ⟶{𝑡}_{𝑛}$。每一步大小至少减 $1$，所以 $\mathrm{size}\left({𝑡}_{𝑛}\right)\le \mathrm{size}\left(𝑡\right)-𝑛$。大小至少为 $1$，故 $𝑛\le \mathrm{size}\left(𝑡\right)-1$。