{aⁿbⁿcⁿ} is context-sensitive

This file constructs the unrestricted grammar grammar_anbncn for {aⁿbⁿcⁿ | n ≥ 1}, proves it generates exactly that language (grammar_anbncn_language), and observes that every rule is non-contracting (grammar_anbncn_noncontracting). Hence the positive language is context-sensitive, and adjoining the empty word n = 0 via is_CS_insert_empty_of_noncontracting yields {aⁿbⁿcⁿ | n ≥ 0} = lang_eq_eq.

Nonterminals: Fin 2 where 0 = S, 1 = B.

Rules:

1. S → a B c
2. S → a S B c
3. c B → B c (bubble sort)
4. a B → a b (context-sensitive conversion)
5. b B → b b (context-sensitive conversion)

Main declarations

• grammar_anbncn_language
• grammar_anbncn_noncontracting
• lang_eq_eq_is_CS

@[reducible]

def grammar_anbncn : grammar (Fin 3)

Equations

• One or more equations did not get rendered due to their size.

theorem grammar_anbncn_language : grammar_language grammar_anbncn = lang_eq_eq_pos

The grammar grammar_anbncn generates exactly {aⁿbⁿcⁿ | n ≥ 1}.

theorem grammar_anbncn_noncontracting : grammar_noncontracting grammar_anbncn

The grammar grammar_anbncn is non-contracting: every rule's output string is at least as long as its full input pattern.

theorem lang_eq_eq_is_CS : is_CS lang_eq_eq

The language {aⁿbⁿcⁿ} is context-sensitive.

grammar_anbncn is non-contracting and generates the positive language {aⁿbⁿcⁿ | n ≥ 1} (grammar_anbncn_language); is_CS_insert_empty_of_noncontracting re-adjoins the empty word n = 0, which is exactly the difference between lang_eq_eq_pos and lang_eq_eq.