Lemma. 值不可规约 Glomzzz 2026-10-10 About 采用 值与数值 的值定义 与 一步规约 的十条求值规则． 若 𝑣 是值，则不存在 𝑡 ′ 使 𝑣⟶𝑡 ′．Proof.对 值与数值 的值作结构归纳． 常量 true、false、0 作为基准情况： 逐条检查十条规则的结论左边，没有一条是这三个常量之一． 对于 succ nv： 结论左边形如 succ … 的规则只有 E-Succ，它的前提要求 nv ⟶ t'_(1)； 而 nv 是更小的值，由 归纳假设 不可能规约．∎
