trans_produces

Mathlib.Computability.ContextFreeGrammar

URI: https://scilib.ai/kg/mathlib#ContextFreeGrammar.Derives.trans_produces

English

If deriving u to v and g.Produces v to w, then derive u to w.

Русский

Если u выводится в v, а v производится в w, то u выводится в w.

LaTeX

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

Lean4

theorem trans_produces {u v w : List (Symbol T g.NT)} (huv : g.Derives u v) (hvw : g.Produces v w) : g.Derives u w :=
  huv.trans hvw.single

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

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

Разделы

Аффилиация

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