eq_or_head — Mathlib

English

From a derivation, either the left side equals the right side, or there exists a single production step from the left to some intermediate, leading to the right.

Русский

Из вывода следует либо совпадение левой и правой частей, либо существует первый шаг вывода, приводящий из левой части к некоторой послковательности, которая далее выводит правую.

LaTeX

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

Lean4

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

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