[引理] 值不可归约 Glomzzz 2026-10-10 About 采用 [定义] 值与数值 的值定义与 [定义] 一步归约 的十条求值规则。若 𝑣 是值，则不存在 𝑡 ′ 使 𝑣⟶𝑡 ′。证明对 [定义] 值与数值 的值做结构归纳。true、false、0：逐条检查十条规则的结论左边，没有一条是这三个常量之一。：结论左边形如 succ … 的规则只有 E-Succ，它的前提要求 。 是更小的值，由 归纳假设 不可能。∎ References [定义] 值与数值 [values-and-numeric-values] [定义] 归纳假设 [induction-hypothesis] [定义] 一步归约 [one-step-reduction] Backlinks [] 范式、受阻与多步归约 [normal-forms] [例] 归约到受阻 [reduction-to-a-stuck-term] [注记] 存在与生成 [being-and-becoming] [定理] 确定性 [determinism] Based on Typsite