English
Copy operation simulates duplicating a portion of the stack during a TM2 step, preserving the original data structure while enabling replication.
Русский
Операция копирования моделирует дублирование части стека во время шага TM2, сохранения исходной структуры данных.
LaTeX
$$$\\text{copy\\_ok} : \\; \\text{Reaches}_1 (\\text{TM2.step } tr)(\\langle \\operatorname{copy}(q) , \\dots\\rangle) \\Rightarrow \\langle q, \\dots \\rangle$$$
Lean4
theorem copy_ok (q s a b c d) :
Reaches₁ (TM2.step tr) ⟨some (Λ'.copy q), s, K'.elim a b c d⟩
⟨some q, none, K'.elim (List.reverseAux b a) [] c (List.reverseAux b d)⟩ :=
by
induction b generalizing a d s with
| nil =>
refine TransGen.single ?_
simp
| cons x b IH =>
refine TransGen.head rfl ?_
rw [tr]
simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some, List.tail_cons,
elim_update_rev, elim_main, elim_update_main, elim_stack, elim_update_stack, cond_true, List.reverseAux_cons,
pop', push']
exact IH _ _ _
