The deterministic context-free language {a^n b^m c^m}

This file gives a deterministic pushdown automaton for {aⁿbᵐcᵐ | n,m ≥ 0} over the Fin 3 alphabet shared with AnBnCm.

inductive DCFLIntersection.AnyEqState : Type

• start : AnyEqState
• seenB : AnyEqState
• seenC : AnyEqState
• matched : AnyEqState

instance DCFLIntersection.instDecidableEqAnyEqState : DecidableEq AnyEqState

Equations

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

instance DCFLIntersection.instFintypeAnyEqState : Fintype AnyEqState

Equations

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

def DCFLIntersection.dpda_any_eq : DPDA AnyEqState (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_any_eq_accepts : dpda_any_eq.acceptsByFinalState = lang_any_eq

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

theorem DCFLIntersection.DCF_lang_any_eq : is_DCF lang_any_eq

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