cons_left_iff — Mathlib

English

No single-letter word [p] can be reduced by a step; Step([p]) L is false when L is arbitrary; single-letter words cannot be reduced by a single step.

Русский

Ни одно одноэлементное слово [p] не может быть сведено шагом; Step([p]) L ложно, когда L произвольна; одноэлементные слова не редуцируются одним шагом.

LaTeX

$$$ \\forall p, \\neg \\mathrm{Step}([p])\\, L$$$

Lean4

@[to_additive]
theorem cons_left_iff {a : α} {b : Bool} :
    Step ((a, b) :: L₁) L₂ ↔ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ :=
  by
  constructor
  · generalize hL : ((a, b) :: L₁ : List _) = L
    rintro @⟨_ | ⟨p, s'⟩, e, a', b'⟩ <;> simp_all
  · rintro (⟨L, h, rfl⟩ | rfl)
    · exact Step.cons h
    · exact Step.cons_not

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