LanglibCNF Bridge Lemmas #
This file adds small bridge lemmas connecting the project's Chomsky-normal-form API to mathlib conventions.
Main declarations #
theorem
ChomskyNormalFormRule.Rewrites.word
{T : Type uT}
{N : Type uN}
{r : ChomskyNormalFormRule T N}
{u : List T}
{v : List (Symbol T N)}
(hruv : r.Rewrites (List.map Symbol.terminal u) v)
:
theorem
ChomskyNormalFormGrammar.Produces.input_output
{T : Type uT}
{g : ChomskyNormalFormGrammar T}
{r : ChomskyNormalFormRule T g.NT}
(hrg : r ∈ g.rules)
: