[定理] 进展

采用 [定义] 类型与类型判断的类型关系、 [定义] 值与数值的值定义，以及 [定义] 一步归约的归约关系。若 $𝑡 : 𝑇$ ，则 $𝑡$ 是值，或存在 $𝑡^{'}$ 使 $𝑡 ⟶ 𝑡^{'}$ 。

证明

对 $𝑡 : 𝑇$ 的推导归纳（类型推导版本的 [定理] 对推导归纳），按最后一步的规则分情形。

T-True、T-False、T-Zero： $𝑡$ 是值。
T-If： $𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ，前提里有 $𝑡_{1} : Bool$ 。对 $𝑡_{1}$ 用归纳假设：
- 若 $𝑡_{1}$ 能归约，用 E-If， $𝑡$ 也能归约；
- 若 $𝑡_{1}$ 是值，由 [引理] 典范形式（canonical forms）第 1 条，它是 $true$ 或 $false$ ，分别用 E-IfTrue、E-IfFalse。
T-Succ：前提 $𝑡_{1} : Nat$ 。若 $𝑡_{1}$ 能归约，用 E-Succ。若 $𝑡_{1}$ 是值，由 [引理] 典范形式（canonical forms）第 2 条它是数值，于是本身也是数值，因而是值。
T-Pred：前提 $𝑡_{1} : Nat$ 。若 $𝑡_{1}$ 能归约，用 E-Pred。若 $𝑡_{1}$ 是值，它是数值：是 $0$ 就用 E-PredZero；否则形如，用 E-PredSucc。
T-IsZero：与 T-Pred 相同，分别用 E-IsZero、E-IsZeroZero、E-IsZeroSucc。

∎

References