Theorem: DA.memAccepts (FOL/Parsing/Compute.lean)

State before:
α σ : Type
D : DA α σ
input : List α
⊢ D.accepts input ↔ D.evalFrom D.startingState input ∈ D.acceptingStates
Tactic:
rfl
State after:
no goals