eq_or_tail — Mathlib

English

From a derivation, either w equals u, or there exists v such that u derives v and v produces w.

Русский

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

LaTeX

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

Lean4

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

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