a^n b^n as an LR Language

This file proves that the context-free grammar cfg_anbn for {a^n b^n} is LR(0), and hence that the language is LR.

Main results

• cfg_anbn_isLRk_zero — the grammar cfg_anbn is LR(0)
• anbn_is_LRk_zero — {a^n b^n} is generated by an LR(0) grammar
• anbn_is_LR — {a^n b^n} is an LR language

Rightmost sentential forms of cfg_anbn

The grammar cfg_anbn has rules S → aSb and S → ε with a single nonterminal (). Every sentential form has at most one nonterminal, so every derivation step is automatically rightmost. The reachable rightmost forms are exactly aⁿ S bⁿ and aⁿ bⁿ.

theorem cfg_anbn_isLRk_zero : cfg_anbn.IsLRk 0

The grammar cfg_anbn is LR(0).

theorem anbn_is_LRk_zero : is_LRk 0 anbn

The language {aⁿbⁿ} is generated by an LR(0) grammar.

theorem anbn_is_LR : is_LR anbn

The language {aⁿbⁿ} is an LR language.