case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ NFA.accepts (toNFA M) ↔ x ∈ accepts M
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
⊢ NFA.accepts (toNFA M) = accepts M
ext x
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) ↔ x ∈ accepts M
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ NFA.accepts (toNFA M) ↔ x ∈ accepts M
rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]
case h.mp
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) → x ∈ accepts M

case h.mpr
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ accepts M → ∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) ↔ x ∈ accepts M
constructor
case h.mp.intro.intro
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ (toNFA M).accept
hS₂ : S ∈ {evalFrom M M.start x}
⊢ x ∈ accepts M
case h.mp
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) → x ∈ accepts M
rintro ⟨S, hS₁, hS₂⟩
no goals
case h.mp.intro.intro
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ (toNFA M).accept
hS₂ : S ∈ {evalFrom M M.start x}
⊢ x ∈ accepts M
rwa [Set.mem_singleton_iff.mp hS₂] at hS₁
no goals
case h.mpr
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ accepts M → ∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}
exact fun h => ⟨M.eval x, h, rfl⟩