English
Under finiteness constraints, if M.evalFrom s x equals t, then there exist a, b, c with x = a ++ b ++ c, a.length + b.length ≤ card σ, b ≠ ∅, and a new evaluation chain through a, b, c reaches t.
Русский
При конечности существует разбиение x = a ++ b ++ c с заданными ограничениями, приводящее к достижению t через оценивающий процесс через a, b, c.
LaTeX
$$$\exists q,a,b,c\,\bigl(x = a ++ b ++ c \land a.Length + b.Length \le |\sigma| \land b \neq \emptyset \land M.evalFrom s a = q \land M.evalFrom q b = q \land M.evalFrom q c = t\bigr)$$$
Lean4
theorem evalFrom_split [Fintype σ] {x : List α} {s t : σ} (hlen : Fintype.card σ ≤ x.length) (hx : M.evalFrom s x = t) :
∃ q a b c,
x = a ++ b ++ c ∧
a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t :=
by
obtain ⟨n, m, hneq, heq⟩ :=
Fintype.exists_ne_map_eq_of_card_lt (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by simp)
wlog hle : (n : ℕ) ≤ m generalizing n m
· exact this m n hneq.symm heq.symm (le_of_not_ge hle)
refine ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
· rw [List.take_append_drop, List.take_append_drop]
· simp only [List.length_drop, List.length_take]
omega
· intro h
have hlen' := congr_arg List.length h
simp only [List.length_drop, List.length, List.length_take] at hlen'
omega
have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) = M.evalFrom s ((x.take m).take n) := by
rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ← List.take_take,
min_eq_left hle, List.take_append_drop]
use hq
rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc, List.take_append_drop,
List.take_append_drop]
