derives_iff_eq_or_tail — Mathlib

English

Derives u w is equivalent to w = u or there exists v with u derives v and v produces w.

Русский

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

LaTeX

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

Lean4

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

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