trans_derives

Mathlib.Computability.ContextFreeGrammar

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

English

If u derives v and v produces w, then u derives 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_derives {u v w : List (Symbol T g.NT)} (huv : g.Produces u v) (hvw : g.Derives v w) : g.Derives u w :=
  huv.single.trans hvw

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

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

Разделы

Аффилиация

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