sizeof_of_step — Mathlib

English

For a one-step reduction, the size of the target is strictly smaller than the source.

Русский

Для одного шага редукции размер целевого слова строго меньше размера исходного.

LaTeX

$$$\text{Step}\;L_1\;L_2 \Rightarrow \text{sizeOf}(L_2) < \text{sizeOf}(L_1)$$$

Lean4

@[to_additive]
theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)}, Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
  | _, _, @Step.not _ L1 L2 x b => by
    induction L1 with
    | nil =>
      dsimp
      cutsat
    | cons hd tl ih =>
      dsimp
      exact Nat.add_lt_add_left ih _

Похожие утверждения