Commit 2025-04-07 12:49 0bd203b3

View on Github →

feat(Computability/CFG): lemmas about nonterminals (#21585) helps with reasoning about CFGs with a language of the empty set

Estimated changes

Modified Mathlib/Computability/ContextFreeGrammar.lean

added theorem ContextFreeGrammar.Produces.exists_nonterminal_input_mem

added theorem ContextFreeGrammar.derives_iff_eq_or_head

added theorem ContextFreeGrammar.derives_iff_eq_or_tail

added theorem ContextFreeGrammar.derives_nonterminal

added theorem ContextFreeGrammar.language_eq_zero_of_forall_input_ne_initial

added theorem ContextFreeRule.Rewrites.nonterminal_input_mem