cases d
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
d : RegularGrammar.RegularDerivation (toGrammar M) s w
⊢ NFA.Run.last (fromDerivation M d) ∈ M.F
case eps
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w✝ : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w✝)) ∈ M.F

case alpha
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v✝ h_w✝)) ∈ M.F

case step
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w✝ : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w✝ a✝)) ∈ M.F