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

State before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
⊢ N.to_DFA.accepts = N.accepts
Tactic:
ext cs
State after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.accepts cs ↔ N.accepts cs

State before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.accepts cs ↔ N.accepts cs
Tactic:
simp only [DFA.mem_accepts]
State after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔ N.accepts cs

State before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔ N.accepts cs
Tactic:
simp only [NFA.mem_accepts]
State after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list

State before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list
Tactic:
simp only [NFA.to_DFA]
State after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ { step := N.eval_one, starting_state := N.starting_state_list,
            accepting_state_list := sorryAx (List (List σ)) }.eval_from
        N.starting_state_list cs ∈
      sorryAx (List (List σ)) ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list

State before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ { step := N.eval_one, starting_state := N.starting_state_list,
            accepting_state_list := sorryAx (List (List σ)) }.eval_from
        N.starting_state_list cs ∈
      sorryAx (List (List σ)) ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list
Tactic:
sorry
State after:
no goals