case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ x ∈ DFA.accepts (toDFA M) ↔ x ∈ accepts M
α : Type u
σ σ' : Type v
M : NFA α σ
⊢ DFA.accepts (toDFA M) = accepts M
ext x
case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept ↔ ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ x ∈ DFA.accepts (toDFA M) ↔ x ∈ accepts M
rw [mem_accepts, DFA.mem_accepts]
no goals
case h.mpr
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ (∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x) → DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩