Theorem: EpsilonNFA.accepts_iff (FOL/Parsing/EpsilonNFA.lean)

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ e.accepts input ↔ e.toAbstract.accepts input
Tactic:
simp [accepts, eval]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list) ↔ e.toAbstract.accepts input

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list) ↔ e.toAbstract.accepts input
Tactic:
rw [EpsilonNFA.eval_from_iff]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.starting_state_list, e.toAbstract.eval s input) ↔ e.toAbstract.accepts input

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.starting_state_list, e.toAbstract.eval s input) ↔ e.toAbstract.accepts input
Tactic:
rfl
State after:
no goals