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

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : NFA α σ
input : List α
⊢ e.accepts input ↔ ∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list
Tactic:
rfl
State after:
no goals