α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ {x | ∃ S, S ∈ (toεNFA M).accept ∧ S ∈ evalFrom M (toεNFA M).start x} = accepts M
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ εNFA.accepts (toεNFA M) = accepts M
rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]
no goals
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ {x | ∃ S, S ∈ (toεNFA M).accept ∧ S ∈ evalFrom M (toεNFA M).start x} = accepts M
rfl