Auxiliary grammar lemmas #
Small facts about ChomskyNormalFormRule.Rewrites and ChomskyNormalFormGrammar.Produces
intended for upstreaming into Mathlib alongside the Chomsky-normal-form development.
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)
: