a^n b^n as a CFL

This file constructs a context-free grammar for {a^n b^n} and proves that the language is context-free.

def cfg_anbn : CF_grammar Bool

Context-free grammar for the language {aⁿbⁿ | n ∈ ℕ} over Bool.

Equations

• cfg_anbn = { nt := Unit, initial := (), rules := [((), [symbol.terminal false, symbol.nonterminal (), symbol.terminal true]), ((), [])] }

theorem CF_language_cfg_anbn : CF_language cfg_anbn = anbn

The grammar cfg_anbn generates exactly {aⁿbⁿ}.

theorem anbn_is_CF : is_CF anbn

The language {aⁿbⁿ} is context-free.