（仅当： 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}$ 同理对应 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) ）对 $𝑡⟶𝑢$ 作规则归纳（ [定理] 规则归纳法（rule induction） ），按最后一步的规则分情形。

• 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}$ 的三条一一对应，论证相同。