LR languages are a strict subclass of context-free languages

Positive-lookahead LR(k), existential-lookahead LR, and deterministic context-free languages are the same language class. Transporting the known strict inclusion DCF ⊊ CF therefore gives the result directly for the LR classes named in the hierarchy table.

theorem LRk_strict_subclass_CF (k : ℕ) (hk : 0 < k) : LRk k ⊂ CF

For every fixed positive k, LR(k) languages form a strict subclass of context-free languages over a three-symbol alphabet.

theorem LRk_strict_subclass_CF_of_card {T : Type} [Fintype T] (k : ℕ) (hk : 0 < k) (hT : 3 ≤ Fintype.card T) : LRk k ⊂ CF

For every fixed positive k, LR(k) languages form a strict subclass of context-free languages over any finite alphabet with at least three symbols.

theorem LR_strict_subclass_CF : LR ⊂ CF

Existential finite-lookahead LR languages form a strict subclass of context-free languages over a three-symbol alphabet.

theorem LR_strict_subclass_CF_of_card {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) : LR ⊂ CF

Existential finite-lookahead LR languages form a strict subclass of context-free languages over any finite alphabet with at least three symbols.