a^n b^n as a DCF

This file constructs a deterministic pushdown automaton for the language {a^n b^n | n >= 0} and proves that this language is deterministic context-free.

def dpda_anbn : DPDA (Fin 4) Bool Bool

DPDA recognizing {aⁿbⁿ | n ≥ 0} where false = a and true = b.

Equations

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

theorem dpda_anbn_accepts : dpda_anbn.acceptsByFinalState = anbn

The DPDA dpda_anbn accepts exactly the language {aⁿbⁿ}.

theorem anbn_is_DCF : is_DCF anbn

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