Theorems · Definition · computer science
DFA.accepts
{α : Type u} → {σ : Type v} → DFA α σ → Language αM.accepts is the language of x such that M.eval x is an accept state.
- Defined in
- Mathlib.Computability.DFA
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Languagestatement · cited by 125
- DFAstatement and proof · cited by 58
- DFA.startproof · cited by 18
- DFA.acceptsFromproof · cited by 9
Cited by19
Results whose statement or proof uses this declaration.
- Language.IsRegularproof · cited by 12
- DFA.mem_acceptsstatement · cited by 4
- Language.IsRegular.complproof · cited by 2
- Language.IsRegular.reverseproof · cited by 2
- NFA.toDFA_correctstatement and proof · cited by 2
- Language.accepts_toDFAstatement · cited by 1
- Language.IsRegular.finite_range_leftQuotientproof · cited by 1
- DFA.pumping_lemmastatement and proof · cited by 1
- DFA.toNFA_correctstatement and proof · cited by 1
- Language.isRegular_iffstatement · cited by 1
- DFA.accepts_interstatement · cited by 1
- DFA.accepts_unionstatement · cited by 1