evalFrom_reindex — Mathlib

English

Evaluating a reindexed DFA on a state s corresponds to applying the renaming g to the evaluation of the original on the preimage state.

Русский

Оценка переиндексированного DFA на состоянии s равна применения g к оценке исходного на обратном образе s.

LaTeX

$$$ (\\mathrm{reindex} g M).\\mathrm{evalFrom} s x = g (M.\\mathrm{evalFrom} (g^{-1} s) x) $$$

Lean4

@[simp]
theorem evalFrom_reindex (g : σ ≃ σ') (s : σ') (x : List α) :
    (reindex g M).evalFrom s x = g (M.evalFrom (g.symm s) x) := by
  induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]

Похожие утверждения