（仅当： step(t) = Some(u) step(t) = Some(u) 蕴涵 $𝑡⟶𝑢$） 对 $𝑡$ 结构归纳，按 step step 实际走到的分支分情形． 常量 $\text{true}$、$\text{false}$、$0$ 上 step step 返回 None None ，前提不成立． 当 $𝑡=\text{ if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3$ 时，若 ${𝑡}_1$ 是 $\text{true}$ 则返回 ${𝑡}_2$（对应 E-IfTrue），若是 $\text{false}$ 则返回 ${𝑡}_3$（对应 E-IfFalse）；否则 step(t1) = Some(t1') step(t1) = Some(t1') 且 $𝑢=\text{ if }{𝑡}_1^{\prime }\text{ then }{𝑡}_2\text{ else }{𝑡}_3$，由 归纳假设 得 ${𝑡}_1⟶{𝑡}_1^{\prime }$，再用 E-If 即得． 当 $𝑡=\text{ succ }{𝑡}_1$ 时， step(t1) = Some(t1') step(t1) = Some(t1') 且 $𝑢=\text{ succ }{𝑡}_1^{\prime }$，由 归纳假设 与 E-Succ 即得． 当 $𝑡=\text{ pred }{𝑡}_1$ 时，若 ${𝑡}_1$ 是 $0$ 则返回 $0$（E-PredZero），若 t_(1) = succ nv（ is_nv is_nv 为真）则返回 nv（E-PredSucc），其余情形 step(t1) = Some(t1') step(t1) = Some(t1') ，由 归纳假设 与 E-Pred 即得． $\text{iszero }{𝑡}_1$ 与 $\text{pred}$ 的三个分支一一对应，分别用 E-IsZeroZero、E-IsZeroSucc、E-IsZero．

（若：$𝑡⟶𝑢$ 蕴涵 step(t) = Some(u) step(t) = Some(u) ） 对 $𝑡⟶𝑢$ 作规则归纳（ 规则归纳法 ）， 按最后一步的规则分情形． 对 E-IfTrue、E-IfFalse，条件分别是 $\text{true}$、$\text{false}$， step step 的前两个分支直接返回 ${𝑡}_2$、${𝑡}_3$． 对 E-If，前提为 ${𝑡}_1⟶{𝑡}_1^{\prime }$；由 值不可规约 知 ${𝑡}_1$ 不属于值，不可能匹配 $\text{true}$ 或 $\text{false}$，所以 step step 走第三个分支，再由 归纳假设 得 step(t1) = Some(t1') step(t1) = Some(t1') ，返回 $\text{if }{𝑡}_1^{\prime }\text{ then }{𝑡}_2\text{ else }{𝑡}_3$． 对 E-Succ，由 归纳假设 直接得到． 对 E-PredZero、E-PredSucc， step step 的前两个分支返回规则的结论，其中 E-PredSucc 的条件 is_nv is_nv 正是规则对 nv 的限制． 对 E-Pred，前提为 ${𝑡}_1⟶{𝑡}_1^{\prime }$；由 值不可规约 知 ${𝑡}_1$ 不属于值，不可能匹配 $0$ 或数值 succ nv， step step 走第三个分支，由 归纳假设 得 step(t1) = Some(t1') step(t1) = Some(t1') ． E-IsZeroZero、E-IsZeroSucc、E-IsZero 与 $\text{pred}$ 的三条一一对应，论证相同．