Theorem: DFA.fromNFA_run_imp_run
Proof state before:
case right.w.x
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ?right.w.q₂ ∈ M.δ (x, ?right.w.a)

case right.w.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M ?right.w.q₂ ?right.w.w

case right.w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ w = ?right.w.a :: ?right.w.w

case right.w.q₂
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ { x // x ∈ M.Q }

case right.w.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ { x // x ∈ M.Z }

case right.w.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ Word { x // x ∈ M.Z }

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last (NFA.Run.step x ?right.w.x ?right.w.r ?right.w.h) ∈ M.F
Tactic:
repeat { assumption }
Proof state after:
no goals