English
If M.evalFrom s x = s and y ∈ {x}^*, then M.evalFrom s y = s; that is, executing along any repetition of x from s remains at s.
Русский
Если вычисление M от s по x возвращает s, и y принадлежит к множеству повторов x, то M.evalFrom s y = s.
LaTeX
$$$ M.\mathrm{evalFrom}(s, x) = s \Rightarrow y \in \{x\}^{*} \Rightarrow M.\mathrm{evalFrom}(s, y) = s $$$
Lean4
theorem evalFrom_of_pow {x y : List α} {s : σ} (hx : M.evalFrom s x = s) (hy : y ∈ ({ x } : Language α)∗) :
M.evalFrom s y = s := by
rw [Language.mem_kstar] at hy
rcases hy with ⟨S, rfl, hS⟩
induction S with
| nil => rfl
| cons a S ih =>
have ha := hS a List.mem_cons_self
rw [Set.mem_singleton_iff] at ha
rw [List.flatten, evalFrom_of_append, ha, hx]
apply ih
intro z hz
exact hS z (List.mem_cons_of_mem a hz)
