α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.evalFrom (toεNFA M) start = evalFrom M start
rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.stepSet (toεNFA M) = stepSet M
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ εNFA.stepSet (toεNFA M) S s ↔ x✝ ∈ stepSet M S s
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.stepSet (toεNFA M) = stepSet M
ext S s
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i, i ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) i (some s))) ↔ ∃ i, i ∈ S ∧ x✝ ∈ step M i s
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ εNFA.stepSet (toεNFA M) S s ↔ x✝ ∈ stepSet M S s
simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ a ∈ S ∧ x✝ ∈ step M a s
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i, i ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) i (some s))) ↔ ∃ i, i ∈ S ∧ x✝ ∈ step M i s
apply exists_congr
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S → (x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ x✝ ∈ step M a s)
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ a ∈ S ∧ x✝ ∈ step M a s
simp only [and_congr_right_iff]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a✝¹ (some s)) ↔ x✝ ∈ step M a✝¹ s
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S → (x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ x✝ ∈ step M a s)
intro _ _
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.step (toεNFA M) a✝¹ (some s) ↔ x✝ ∈ step M a✝¹ s
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a✝¹ (some s)) ↔ x✝ ∈ step M a✝¹ s
rw [M.toεNFA_εClosure]
no goals
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.step (toεNFA M) a✝¹ (some s) ↔ x✝ ∈ step M a✝¹ s
rfl
no goals
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
this : εNFA.stepSet (toεNFA M) = stepSet M
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
rw [this]