derives_iff_eq_or_head — Mathlib

English

Derives u w holds exactly when either u = w or there exists v such that u produces v and v derives w.

Русский

Выводы между u и w существуют тогда, когда либо u = w, либо существует v, для которого u производит v и v выводится в w.

LaTeX

$$$g.Derives\ u\ w \iff \; u = w \lor \exists v,\ g.Produces\ u\ v \wedge g.Derives\ v\ w$$$

Lean4

theorem derives_iff_eq_or_head {u w : List (Symbol T g.NT)} :
    g.Derives u w ↔ u = w ∨ ∃ v : List (Symbol T g.NT), g.Produces u v ∧ g.Derives v w :=
  Relation.ReflTransGen.cases_head_iff

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