Theorem: DFA.mem_accepts (FOL/Parsing/DFA.lean)

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
D : DFA α σ
input : List α
⊢ D.accepts input ↔ D.eval_from D.starting_state input ∈ D.accepting_state_list
Tactic:
rfl
State after:
no goals