English
For a DFA M and a start state, evaluating from a word is preserved under the conversion to an NFA: the set of reachable states after reading a word equals the singleton set containing the DFA's evaluation.
Русский
Для DFA M и начального состояния сохранено равенство множеств достижимых состояний после чтения слова при переходе к NFA: множество достижимых после чтения равно одиночному множеству, содержащему вычисление DFA.
LaTeX
$$$M.toNFA.evalFrom \{ start \} s = \{ M.evalFrom start s \}$$$
Lean4
@[simp]
theorem toNFA_evalFrom_match (M : DFA α σ) (start : σ) (s : List α) :
M.toNFA.evalFrom { start } s = {M.evalFrom start s} :=
by
change List.foldl M.toNFA.stepSet { start } s = {List.foldl M.step start s}
induction s generalizing start with
| nil => tauto
| cons a s
ih =>
rw [List.foldl, List.foldl, show M.toNFA.stepSet { start } a = {M.step start a} by simp [NFA.stepSet]]
tauto
