single

Mathlib.Computability.ContextFreeGrammar

URI: https://scilib.ai/kg/mathlib#ContextFreeGrammar.Produces.single

English

If a sequence v can be produced from u by g.Produces, then u Derives v in zero or more steps.

Русский

Если из u можно получить v через g.Produces, то u выводится к v за конечное число шагов.

LaTeX

$$$\forall v\forall w,\; g.Produces\, v\, w \Rightarrow g.Derives\, v\, w$$$

Lean4

theorem single {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) : g.Derives v w :=
  Relation.ReflTransGen.single hvw

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru