of_forall_not_step — Mathlib

English

If L1 has no reduction step to any L2, then L1 is reduced.

Русский

Если у слова L1 нет ни одного редукционного шага к любому L2, то L1 редуцировано.

LaTeX

$$$\forall L_1,\ (\forall L_2, \neg Red.Step(L_1,L_2)) \rightarrow \operatorname{IsReduced}(L_1).$$$

Lean4

@[to_additive]
theorem of_forall_not_step : ∀ {L₁ : List (α × Bool)}, (∀ L₂, ¬Red.Step L₁ L₂) → IsReduced L₁
  | [], _ => .nil
  | [a], _ => .singleton
  | (a₁, b₁) :: (a₂, b₂) :: L₁, hL₁ => by
    rw [isReduced_cons_cons]
    refine ⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩
    rintro rfl
    symm
    rw [← Bool.ne_not]
    rintro rfl
    exact hL₁ L₁ <| .not (L₁ := [])

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