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

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈ e.eval_one_no_eps starting_state_list symbol ↔
    ∃ state ∈ starting_state_list, stop_state ∈ symbol_arrow_list_to_fun e.symbol_arrow_list state symbol
Tactic:
simp only [eval_one_no_eps]
State after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, stop_state ∈ symbol_arrow_list_to_fun e.symbol_arrow_list state symbol

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, stop_state ∈ symbol_arrow_list_to_fun e.symbol_arrow_list state symbol
Tactic:
simp
State after:
no goals