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(1), and hence that the language is LR.

Main results

• cfg_anbn_isLRk_one — the grammar cfg_anbn is LR(1)
• anbn_is_LRk_one — {a^n b^n} is generated by an LR(1) 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_one : cfg_anbn.IsLRk 1

The grammar cfg_anbn is LR(1).

theorem anbn_is_LRk_one : is_LRk 1 anbn

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

theorem anbn_is_LR : is_LR anbn

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