constructor
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F