Deterministic Context-Free Examples over a b c

This file gives a deterministic pushdown automaton for {aⁿbⁿcᵐ | n,m ≥ 0}.

inductive DCFLIntersection.EqAnyState : Type

• start : EqAnyState
• seenA : EqAnyState
• seenB : EqAnyState
• trailC : EqAnyState
• onlyC : EqAnyState

instance DCFLIntersection.instDecidableEqEqAnyState : DecidableEq EqAnyState

Equations

• DCFLIntersection.instDecidableEqEqAnyState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DCFLIntersection.instFintypeEqAnyState : Fintype EqAnyState

Equations

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

def DCFLIntersection.dpda_eq_any : DPDA EqAnyState (Fin 3) ABCStack

DPDA recognizing {aⁿbⁿcᵐ | n,m ≥ 0}.

Equations

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

theorem DCFLIntersection.dpda_eq_any_accepts : dpda_eq_any.acceptsByFinalState = lang_eq_any

The dpda_eq_any automaton recognizes {aⁿbⁿcᵐ | n,m ≥ 0}.

theorem DCFLIntersection.DCF_lang_eq_any : is_DCF lang_eq_any

The first witness language {aⁿbⁿcᵐ | n,m ≥ 0} is deterministic context-free.