From 6e974cdcd4deceddf5556f0b721485786d9df449 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 26 Jan 2026 22:21:47 +0100
Subject: [PATCH 01/21] equal

---
 Complexity/Basic.lean |   1 +
 Complexity/Eq.lean    | 110 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 111 insertions(+)
 create mode 100644 Complexity/Eq.lean

diff --git a/Complexity/Basic.lean b/Complexity/Basic.lean
index b5a64a4..47c4737 100644
--- a/Complexity/Basic.lean
+++ b/Complexity/Basic.lean
@@ -1,6 +1,7 @@
 import Complexity.Bounds
 import Complexity.Classes
 import Complexity.Dyadic
+import Complexity.Eq
 import Complexity.MoveUntil
 import Complexity.SpaceInTime
 import Complexity.Successor
diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
new file mode 100644
index 0000000..557a66c
--- /dev/null
+++ b/Complexity/Eq.lean
@@ -0,0 +1,110 @@
+import Complexity.TuringMachine
+import Complexity.Dyadic
+import Complexity.TapeLemmas
+import Complexity.AbstractTape
+import Complexity.While
+import Complexity.Routines
+
+import Mathlib
+
+-- state 0:
+-- if both separator, move to state 2
+-- as long as equal, move both right and keep in state 0
+-- if different, move to state 3
+-- if
+
+--- A 3-tape Turing machine that pushes the new word "1"
+--- to the third tape if the first words on the first tape are the same
+--- and otherwise pushes the empty word to the third tape.
+
+--- Core of the equality routine: The head of the third tape is on an
+--- empty cell, left of a separator cell. The two first heads check equality.
+--- If the two heads both read separators, the third head writes "1".
+--- If they read two other equal symbols, both move right, and we continue.
+--- If they read two different symbols, the third head moves right.
+def eq_core : TM 3 (Fin 2) SChar :=
+  let σ := fun state symbols =>
+    match state, (symbols 0), (symbols 1) with
+    | 0, .sep, .sep => (1, [(SChar.sep, none), (.sep, .none), ('1', .none)].get)
+    | 0, a, b => if a = b then
+          (0, [(a, .some .right), (a, .some .right), (.blank, none)].get)
+        else
+          (1, [(a, .none), (b, .none), (.blank, .some .right)].get)
+    | 1, _, _ => (1, (symbols ·, none))
+  TM.mk σ 0 1
+
+lemma eq_core.is_inert_after_stop : eq_core.inert_after_stop := by
+  intro conf h_is_stopped
+  ext <;> simp_all [Transition.step, performTapeOps, eq_core]
+
+lemma eq_core_step_separators (l₁ l₂ r₁ r₂ r₃ : List SChar) :
+  eq_core.transforms
+    [.mk₂ l₁ (.sep :: r₁), .mk₂ l₂ (.sep :: r₂), .mk₁ (.blank :: r₃)].get
+    [.mk₂ l₁ (.sep :: r₁), .mk₂ l₂ (.sep :: r₂), .mk₁ ('1' :: r₃)].get := by
+  apply TM.transforms_of_inert eq_core _ _ eq_core.is_inert_after_stop ?_
+  use 1
+  ext1
+  · simp [eq_core, TM.configurations, Transition.step, Turing.Tape.mk₁,
+          Turing.Tape.mk₂, performTapeOps]
+  · dsimp
+    funext i
+    match i with
+    | 0 | 1 | 2 => simp [eq_core, TM.configurations, Transition.step, Turing.Tape.mk₁,
+                         Turing.Tape.mk₂, performTapeOps]
+
+lemma eq_core_step_equal (a : SChar) (h_neq : a ≠ .sep) (l₁ l₂ r₁ r₂ r₃ : List SChar) :
+  eq_core.transition.step
+    ⟨0, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (a :: r₂), .mk₁ (.blank :: r₃)].get⟩ =
+    ⟨0, [.mk₂ (a :: l₁) r₁, .mk₂ (a :: l₂) r₂, .mk₁ (.blank :: r₃)].get⟩ := by
+  ext1
+  · simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₁, Turing.Tape.mk₂, performTapeOps]
+  · dsimp
+    funext i
+    match i with
+    | 0 | 1 | 2 =>
+      simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₁, Turing.Tape.mk₂, performTapeOps]
+
+lemma eq_core_step_non_equal
+  (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
+  (l₁ l₂ r₁ r₂ r₃ : List SChar) :
+  eq_core.transition.step
+    ⟨0, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₁ (.blank :: r₃)].get⟩ =
+    ⟨1, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₁ r₃].get⟩ := by
+  have h_blank_default : SChar.blank = default := rfl
+  ext1
+  · simp [h_neq₁, h_neq₂, h_neq₃, eq_core, Transition.step, Turing.Tape.mk₁,
+          Turing.Tape.mk₂, performTapeOps]
+  · dsimp
+    funext i
+    match i with
+    | 0 | 1 | 2 =>
+      simp [h_blank_default, h_neq₁, h_neq₂, h_neq₃, eq_core,
+            Transition.step, Turing.Tape.mk₁, Turing.Tape.mk₂, performTapeOps]
+
+
+-- def Routines.eq_core : TM 3 (Fin 2) SChar :=
+--   let σ := fun state symbols =>
+--     match state, (symbols 0), (symbols 1) with
+--     | 0, .sep, .sep => (1, (symbols ·, some dir))
+--     | 1, a, b => (1, (symbols ·, none))
+--   TM.mk σ 0 1
+
+-- lemma Routines.move.inert_after_stop {Γ} [Inhabited Γ]
+--   (dir : Turing.Dir) :
+--   (Routines.move (Γ := Γ) dir).inert_after_stop := by
+--   intro conf h_is_stopped
+--   ext <;> simp_all [Transition.step, performTapeOps, Routines.move]
+
+-- lemma Routines.move.semantics {Γ} [Inhabited Γ] [DecidableEq Γ]
+--   {tape : Turing.Tape Γ} {dir : Turing.Dir} :
+--   (Routines.move dir).transforms (fun _ => tape) (fun _ => Turing.Tape.move dir tape) := by
+--   let tm := Routines.move (Γ := Γ) dir
+--   exact TM.transforms_of_inert tm _ _ (move.inert_after_stop dir) ⟨1, rfl⟩
+
+-- @[simp]
+-- lemma Routines.move.eval {Γ} [Inhabited Γ] [DecidableEq Γ]
+--   (tape : Turing.Tape Γ)
+--   (dir : Turing.Dir) :
+--   (Routines.move dir).eval (fun _ => tape) =
+--     .some (fun _ => Turing.Tape.move dir tape) :=
+--   TM.eval_of_transforms Routines.move.semantics

From 7ce1a3ec5193a8acf9d4db5e34c97a22c2f11f41 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 10:17:32 +0100
Subject: [PATCH 02/21] eq

---
 Complexity/Eq.lean            | 118 +++++++++++++++++++---------------
 Complexity/TuringMachine.lean |  13 ++++
 2 files changed, 80 insertions(+), 51 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 557a66c..5f3e0d4 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -7,16 +7,6 @@ import Complexity.Routines
 
 import Mathlib
 
--- state 0:
--- if both separator, move to state 2
--- as long as equal, move both right and keep in state 0
--- if different, move to state 3
--- if
-
---- A 3-tape Turing machine that pushes the new word "1"
---- to the third tape if the first words on the first tape are the same
---- and otherwise pushes the empty word to the third tape.
-
 --- Core of the equality routine: The head of the third tape is on an
 --- empty cell, left of a separator cell. The two first heads check equality.
 --- If the two heads both read separators, the third head writes "1".
@@ -38,73 +28,99 @@ lemma eq_core.is_inert_after_stop : eq_core.inert_after_stop := by
   ext <;> simp_all [Transition.step, performTapeOps, eq_core]
 
 lemma eq_core_step_separators (l₁ l₂ r₁ r₂ r₃ : List SChar) :
-  eq_core.transforms
-    [.mk₂ l₁ (.sep :: r₁), .mk₂ l₂ (.sep :: r₂), .mk₁ (.blank :: r₃)].get
-    [.mk₂ l₁ (.sep :: r₁), .mk₂ l₂ (.sep :: r₂), .mk₁ ('1' :: r₃)].get := by
-  apply TM.transforms_of_inert eq_core _ _ eq_core.is_inert_after_stop ?_
-  use 1
+  eq_core.transition.step
+    ⟨eq_core.startState, [.mk₂ l₁ (.sep :: r₁), .mk₂ l₂ (.sep :: r₂), .mk₂ [] (.blank :: r₃)].get⟩ =
+    ⟨eq_core.stopState, [.mk₂ l₁ (.sep :: r₁), .mk₂ l₂ (.sep :: r₂), .mk₂ [] ('1' :: r₃)].get⟩ := by
   ext1
-  · simp [eq_core, TM.configurations, Transition.step, Turing.Tape.mk₁,
-          Turing.Tape.mk₂, performTapeOps]
+  · simp [eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
   · dsimp
     funext i
     match i with
-    | 0 | 1 | 2 => simp [eq_core, TM.configurations, Transition.step, Turing.Tape.mk₁,
-                         Turing.Tape.mk₂, performTapeOps]
+    | 0 | 1 | 2 => simp [eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
 
 lemma eq_core_step_equal (a : SChar) (h_neq : a ≠ .sep) (l₁ l₂ r₁ r₂ r₃ : List SChar) :
   eq_core.transition.step
-    ⟨0, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (a :: r₂), .mk₁ (.blank :: r₃)].get⟩ =
-    ⟨0, [.mk₂ (a :: l₁) r₁, .mk₂ (a :: l₂) r₂, .mk₁ (.blank :: r₃)].get⟩ := by
+    ⟨eq_core.startState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (a :: r₂), .mk₂ [] (.blank :: r₃)].get⟩ =
+    ⟨eq_core.startState, [.mk₂ (a :: l₁) r₁, .mk₂ (a :: l₂) r₂, .mk₂ [] (.blank :: r₃)].get⟩ := by
   ext1
-  · simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₁, Turing.Tape.mk₂, performTapeOps]
+  · simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
   · dsimp
     funext i
     match i with
     | 0 | 1 | 2 =>
-      simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₁, Turing.Tape.mk₂, performTapeOps]
+      simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
 
 lemma eq_core_step_non_equal
   (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
   (l₁ l₂ r₁ r₂ r₃ : List SChar) :
   eq_core.transition.step
-    ⟨0, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₁ (.blank :: r₃)].get⟩ =
-    ⟨1, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₁ r₃].get⟩ := by
+    ⟨eq_core.startState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₂ [] (.blank :: r₃)].get⟩ =
+    ⟨eq_core.stopState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₂ [] r₃].get⟩ := by
   have h_blank_default : SChar.blank = default := rfl
   ext1
-  · simp [h_neq₁, h_neq₂, h_neq₃, eq_core, Transition.step, Turing.Tape.mk₁,
-          Turing.Tape.mk₂, performTapeOps]
+  · simp [h_neq₁, h_neq₂, h_neq₃, eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
   · dsimp
     funext i
     match i with
     | 0 | 1 | 2 =>
       simp [h_blank_default, h_neq₁, h_neq₂, h_neq₃, eq_core,
-            Transition.step, Turing.Tape.mk₁, Turing.Tape.mk₂, performTapeOps]
+            Transition.step, Turing.Tape.mk₂, performTapeOps]
 
+lemma eq_core_steps_equal
+  (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
+  eq_core.transition.step^[r.length]
+    ⟨eq_core.startState, [.mk₂ l (r ++ r₁), .mk₂ l (r ++ r₂), .mk₂ [] (.blank :: r₃)].get⟩ =
+    ⟨eq_core.startState, [
+      .mk₂ (r.reverse ++ l) r₁,
+      .mk₂ (r.reverse ++ l) r₂,
+      .mk₂ [] (.blank :: r₃)].get⟩ := by
+  induction r generalizing l with
+  | nil => rfl
+  | cons c r ih =>
+    simp only [List.length_cons, List.cons_append, Function.iterate_succ, Function.comp_apply]
+    rw [eq_core_step_equal c (by aesop) l l (r ++ r₁) (r ++ r₂) r₃]
+    rw [ih (c :: l) (by aesop)]
+    simp only [Configuration.mk.injEq, true_and]
+    funext
+    simp
 
--- def Routines.eq_core : TM 3 (Fin 2) SChar :=
---   let σ := fun state symbols =>
---     match state, (symbols 0), (symbols 1) with
---     | 0, .sep, .sep => (1, (symbols ·, some dir))
---     | 1, a, b => (1, (symbols ·, none))
---   TM.mk σ 0 1
+lemma eq_core_eval_different
+  (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
+  (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
+  eq_core.eval [.mk₂ l (r ++ (a :: r₁)), .mk₂ l (r ++ (b :: r₂)), .mk₂ [] (.blank :: r₃)].get =
+    Part.some [
+      .mk₂ (r.reverse ++ l) (a :: r₁),
+      .mk₂ (r.reverse ++ l) (b :: r₂),
+      .mk₂ [] r₃].get := by
+  have h_start_state : eq_core.startState = 0 := rfl
+  apply TM.eval_of_transforms
+  apply TM.transforms_of_inert _ _ _ eq_core.is_inert_after_stop
+  use r.length.succ
+  simp only [TM.configurations, Function.iterate_succ_apply']
+  rw [eq_core_steps_equal l r (a :: r₁) (b :: r₂) r₃ h_r_non_sep]
+  rw [eq_core_step_non_equal a b h_neq₁ h_neq₂ h_neq₃ (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
 
--- lemma Routines.move.inert_after_stop {Γ} [Inhabited Γ]
---   (dir : Turing.Dir) :
---   (Routines.move (Γ := Γ) dir).inert_after_stop := by
---   intro conf h_is_stopped
---   ext <;> simp_all [Transition.step, performTapeOps, Routines.move]
+lemma eq_core_eval_same
+  (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
+  eq_core.eval [.mk₂ l (r ++ .sep :: r₁), .mk₂ l (r ++ .sep :: r₂), .mk₂ [] (.blank :: r₃)].get =
+    Part.some [
+      .mk₂ (r.reverse ++ l) (.sep :: r₁),
+      .mk₂ (r.reverse ++ l) (.sep :: r₂),
+      .mk₂ [] ('1' :: r₃)].get := by
+  have h_start_state : eq_core.startState = 0 := rfl
+  apply TM.eval_of_transforms
+  apply TM.transforms_of_inert _ _ _ eq_core.is_inert_after_stop
+  use r.length.succ
+  simp only [TM.configurations, Function.iterate_succ_apply']
+  rw [eq_core_steps_equal l r (.sep :: r₁) (.sep :: r₂) r₃ h_r_non_sep]
+  rw [eq_core_step_separators (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
 
--- lemma Routines.move.semantics {Γ} [Inhabited Γ] [DecidableEq Γ]
---   {tape : Turing.Tape Γ} {dir : Turing.Dir} :
---   (Routines.move dir).transforms (fun _ => tape) (fun _ => Turing.Tape.move dir tape) := by
---   let tm := Routines.move (Γ := Γ) dir
---   exact TM.transforms_of_inert tm _ _ (move.inert_after_stop dir) ⟨1, rfl⟩
+--- A 3-tape Turing machine that pushes the new word "1"
+--- to the third tape if the first words on the first tape are the same
+--- and otherwise pushes the empty word to the third tape.
 
--- @[simp]
--- lemma Routines.move.eval {Γ} [Inhabited Γ] [DecidableEq Γ]
---   (tape : Turing.Tape Γ)
---   (dir : Turing.Dir) :
---   (Routines.move dir).eval (fun _ => tape) =
---     .some (fun _ => Turing.Tape.move dir tape) :=
---   TM.eval_of_transforms Routines.move.semantics
+-- move left on the third tape
+-- run core
+-- run "move_to_start" on first tape
+-- run "move_to_start" on second tape
+-- def Routines.eq :=
diff --git a/Complexity/TuringMachine.lean b/Complexity/TuringMachine.lean
index 496ca31..9ce3a9b 100644
--- a/Complexity/TuringMachine.lean
+++ b/Complexity/TuringMachine.lean
@@ -252,6 +252,19 @@ lemma TM.transforms_of_inert {k : ℕ} {Q Γ : Type*}
       rw [h_stops_with_tapes₁]
     exact absurd (h_stops_at_t) (Nat.find_min h_stops h_gt)
 
+lemma TM.eval_of_inert {k : ℕ} {Q Γ : Type*}
+  [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q]
+  {tm : TM k Q Γ}
+  {tapes : Fin k → Turing.Tape Γ}
+  (h_inert_after_stop : tm.inert_after_stop)
+  {t : ℕ}
+  (h_stops : (tm.configurations tapes t).state = tm.stopState) :
+  tm.eval tapes = Part.some (tm.configurations tapes t).tapes := by
+  apply TM.eval_of_transforms
+  convert TM.transforms_of_inert _ _ _ h_inert_after_stop ?_
+  use t
+  ext1 <;> simp [h_stops]
+
 def TM.initial_configuration {k : Nat} {S} {Γ}
   (tm : TM k S (Option Γ)) (input : List Γ) : Configuration k S (Option Γ) :=
   let firstTape := Turing.Tape.mk₁ (input.map some)

From 768ff543ce1280376ebf3e8f37cd4e2c11cb2a38 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 11:09:26 +0100
Subject: [PATCH 03/21] move to start

---
 Complexity/MoveUntil.lean  | 36 +++++++++++++++++++++++++++++++++---
 Complexity/TapeLemmas.lean |  8 ++++++++
 2 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/Complexity/MoveUntil.lean b/Complexity/MoveUntil.lean
index 8734800..bf6a345 100644
--- a/Complexity/MoveUntil.lean
+++ b/Complexity/MoveUntil.lean
@@ -4,6 +4,7 @@ import Complexity.TapeLemmas
 import Complexity.AbstractTape
 import Complexity.While
 import Complexity.Routines
+import Complexity.TMComposition
 
 import Mathlib
 
@@ -114,7 +115,7 @@ theorem move_until.left_till_blank {Γ} [Inhabited Γ] [DecidableEq Γ]
   (l : List Γ)
   (n : ℕ)
   (h_nlt : n < l.length)
-  (h_non_blank : ∀ i : Fin l.length, i ≤ n → l.get i ≠ default) :
+  (h_non_blank : ∀ i : ℕ, (h_le : i ≤ n) → l[i] ≠ default) :
   (move_until .left (fun c => c = default)).transforms
     (fun _ => (Turing.Tape.move .right)^[n] (Turing.Tape.mk₁ l))
     (fun _ => (Turing.Tape.mk₁ l).move .left) := by
@@ -136,8 +137,7 @@ theorem move_until.left_till_blank {Γ} [Inhabited Γ] [DecidableEq Γ]
       have h_n'_le_n: n' ≤ n := by omega
       have h_neg_n'_add_n: (-(n': ℤ) + (n : ℤ)).toNat = n - n' := by omega
       have h_n_sub_n'_lt_length : n - n' < l.length := by omega
-      simpa [h_neg_n'_add_n, h_n'_le_n, h_n_sub_n'_lt_length] using
-        h_non_blank ⟨n - n', by omega⟩ (by simp)
+      simp_all
   rw [h_stop_eq]
   simp [move_right_iter_eq_move_int, Turing.Tape.mk₁, ←move_int_neg_one]
 
@@ -154,3 +154,33 @@ lemma move_until.right_till_separator_list
   · have h_len: ↑w.length = Int.ofNat w.coe_schar.length := by simp
     rw [List.coe_schar_length]
     simp only [h_len, move_int_nonneg, Tape.move_right_append, List.append_nil]
+
+def Routines.move_to_start :=
+  (move_until .left (fun c => c = SChar.blank)).seq (Routines.move .right)
+
+theorem Routines.move_to_start_eval
+  {c : SChar} {l r : List SChar}
+  (h_c_non_blank : c ≠ .blank)
+  (h_l_non_blank : .blank ∉ l) :
+  Routines.move_to_start.eval (fun _ => Turing.Tape.mk₂ l (c :: r)) =
+    Part.some (fun _ => Turing.Tape.mk₂ [] (l.reverse ++ (c :: r))) := by
+  have h_blank_default : default = SChar.blank := rfl
+  apply TM.eval_of_transforms
+  apply TM.seq.semantics
+      (tapes₁ := (fun _ => (Turing.Tape.mk₁ (l.reverse ++ (c :: r))).move .left))
+  · convert move_until.left_till_blank
+      (l.reverse ++ (c :: r))
+      l.length
+      (by aesop)
+      ?_
+    · simp [Turing.Tape.mk₁]
+    · intro i h_i
+      have : (l.reverse ++ c :: r) = (c :: l).reverse ++ r := by simp
+      simp only [this]
+      rw [List.getElem_append_left (by grind)]
+      rw [h_blank_default]
+      by_cases h : i < l.reverse.length
+      · simp [List.getElem_append_left h]; grind
+      · grind
+  · convert Routines.move.semantics (dir := .right) (Γ := SChar)
+    simp [Turing.Tape.mk₁]
diff --git a/Complexity/TapeLemmas.lean b/Complexity/TapeLemmas.lean
index 52246f6..468fa41 100644
--- a/Complexity/TapeLemmas.lean
+++ b/Complexity/TapeLemmas.lean
@@ -126,6 +126,14 @@ lemma Tape.move_right_append {Γ} [Inhabited Γ] (A B C : List Γ) :
       _ = Turing.Tape.mk₂ (B.reverse ++ (b :: A)) C := by rw [ih]
       _ = Turing.Tape.mk₂ ((b :: B).reverse ++ A) C := by simp
 
+@[simp]
+lemma Tape.move_right_reverse_append {Γ} [Inhabited Γ] (A B C : List Γ) :
+  (Turing.Tape.move .right)^[B.length] (Turing.Tape.mk₂ A (B.reverse ++ C)) =
+     Turing.Tape.mk₂ (B ++ A) C := by
+  have : B.length = B.reverse.length := by simp
+  rw [this]
+  simpa using Tape.move_right_append A B.reverse C
+
 theorem Tape.left₀_nth {Γ} [Inhabited Γ] (tape : Turing.Tape Γ) (n : ℕ) :
   tape.left₀.nth n = tape.nth (-n) := by
   cases n with

From 4a63fb08dace29006954650df16f13c603c57d5f Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 12:20:17 +0100
Subject: [PATCH 04/21] statement of eq

---
 Complexity/Eq.lean        | 21 ++++++++++++++++++++-
 Complexity/MoveUntil.lean |  1 +
 Complexity/WithTapes.lean |  6 ++++--
 3 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 5f3e0d4..8b4116f 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -4,6 +4,9 @@ import Complexity.TapeLemmas
 import Complexity.AbstractTape
 import Complexity.While
 import Complexity.Routines
+import Complexity.WithTapes
+import Complexity.TMComposition
+import Complexity.MoveUntil
 
 import Mathlib
 
@@ -119,8 +122,24 @@ lemma eq_core_eval_same
 --- to the third tape if the first words on the first tape are the same
 --- and otherwise pushes the empty word to the third tape.
 
+-- push empty word on the third tape
 -- move left on the third tape
 -- run core
 -- run "move_to_start" on first tape
 -- run "move_to_start" on second tape
--- def Routines.eq :=
+def Routines.eq :=
+  (((((cons_empty.seq (Routines.move .left)).with_tapes #v[2]) : TM 3 _ _).seq
+    eq_core).seq
+  (Routines.move_to_start.with_tapes #v[0])).seq
+  (Routines.move_to_start.with_tapes #v[1])
+
+@[simp]
+theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃: List (List Char)) :
+  Routines.eq.eval (list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ws₃].get) =
+    Part.some (if h: w₁ = w₂ then
+      list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ['1'] :: ws₃].get
+    else
+      list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, [] :: ws₃].get) := by
+  by_cases h : w₁ = w₂
+  · sorry
+  · sorry
diff --git a/Complexity/MoveUntil.lean b/Complexity/MoveUntil.lean
index bf6a345..3c785cf 100644
--- a/Complexity/MoveUntil.lean
+++ b/Complexity/MoveUntil.lean
@@ -158,6 +158,7 @@ lemma move_until.right_till_separator_list
 def Routines.move_to_start :=
   (move_until .left (fun c => c = SChar.blank)).seq (Routines.move .right)
 
+@[simp]
 theorem Routines.move_to_start_eval
   {c : SChar} {l r : List SChar}
   (h_c_non_blank : c ≠ .blank)
diff --git a/Complexity/WithTapes.lean b/Complexity/WithTapes.lean
index 946b1f9..e73f1a9 100644
--- a/Complexity/WithTapes.lean
+++ b/Complexity/WithTapes.lean
@@ -19,8 +19,10 @@ def TM.permute_tapes {k : ℕ} {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ]
 --- machine's tape 1
 --- Note that `seq` should not have repetitions.
 --- TODO maybe `seq` should be an injection from Fin k₁ to Fin k₂, then it would be `#v[2, 4].get`.
-def TM.with_tapes {k₁ k₂ : ℕ} {h_le : k₁ ≤ k₂} {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ]
-  (tm : TM k₁ Q Γ) (seq : Vector (Fin k₂) k₁) : TM k₂ Q Γ :=
+def TM.with_tapes {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ]
+  {k₁ k₂ : ℕ}
+  (tm : TM k₁ Q Γ) (seq : Vector (Fin k₂) k₁)
+  (h_le : k₁ ≤ k₂ := by omega) : TM k₂ Q Γ :=
   (seq.mapFinIdx fun i t _ => ((⟨i, by omega⟩ : Fin k₂), t)
     ).foldl (fun tm (a, b) => tm.permute_tapes (Equiv.swap a b)) (tm.extend h_le)
 

From cecd35178b84480341dac05b61e4de13722e6e49 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 13:57:49 +0100
Subject: [PATCH 05/21] eval_ext

---
 Complexity/Eq.lean            | 23 ++++++++++++++++++++---
 Complexity/Routines.lean      |  6 ++++++
 Complexity/TuringMachine.lean | 16 ++++++++++++++++
 3 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 8b4116f..ca9d111 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -134,12 +134,29 @@ def Routines.eq :=
   (Routines.move_to_start.with_tapes #v[1])
 
 @[simp]
-theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃: List (List Char)) :
+theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char)) :
   Routines.eq.eval (list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ws₃].get) =
     Part.some (if h: w₁ = w₂ then
       list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ['1'] :: ws₃].get
     else
       list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, [] :: ws₃].get) := by
+  have h_blank_is_default: SChar.blank = default := rfl
+  have h_part1 : (((cons_empty.seq (Routines.move .left)).with_tapes #v[2]) : TM 3 _ _).eval
+      (list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ws₃].get) =
+      Part.some ([
+        list_to_tape (w₁ :: ws₁),
+        list_to_tape (w₂ :: ws₂),
+        .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get) := by
+    -- TODO create a therem that moves the `.get i` into the `Part.some`?
+    simp only [Fin.isValue, TM.with_tapes.eval_1, Nat.succ_eq_add_one, Nat.reduceAdd,
+      Function.comp_apply, List.get_eq_getElem, List.length_cons, List.length_nil,
+      Fin.coe_ofNat_eq_mod, Nat.mod_succ, List.getElem_cons_succ, List.getElem_cons_zero,
+      TM.seq.eval, cons_empty_eval, Part.bind_some, move.eval, Part.map_some, Part.some_inj]
+    funext i
+    match i with
+    | 0 | 1 | 2 =>
+      simp [Turing.Tape.mk₁, h_blank_is_default, list_to_tape, Turing.Tape.mk₂]
+
   by_cases h : w₁ = w₂
-  · sorry
-  · sorry
+  · simp [h]; sorry
+  · simp [h]; sorry
diff --git a/Complexity/Routines.lean b/Complexity/Routines.lean
index ac40134..4ccfcd9 100644
--- a/Complexity/Routines.lean
+++ b/Complexity/Routines.lean
@@ -189,6 +189,12 @@ theorem cons_empty_semantics (ws : List (List Char)) :
     cons_empty_inert_after_stop
     ⟨2, cons_empty_two_steps ws⟩
 
+@[simp]
+theorem cons_empty_eval (ws : List (List Char)) :
+  cons_empty.eval (fun _ => list_to_tape ws) =
+    .some (fun _ => list_to_tape ([] :: ws)) :=
+  TM.eval_of_transforms (cons_empty_semantics ws)
+
 --- Prepend a character to the first word of the first tape.
 def cons_char (c : Char) :
   TM 1 (Fin 3) SChar :=
diff --git a/Complexity/TuringMachine.lean b/Complexity/TuringMachine.lean
index 9ce3a9b..a700df8 100644
--- a/Complexity/TuringMachine.lean
+++ b/Complexity/TuringMachine.lean
@@ -77,6 +77,22 @@ def TM.eval {k : ℕ} {Q Γ : Type*}
   (PartENat.find (fun t => (tm.configurations tapes t).state = tm.stopState)).map
     fun t => (tm.configurations tapes t).tapes
 
+lemma TM.eval_tapes_ext {k : ℕ} {Q Γ : Type*}
+  [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q]
+  (tm : TM k.succ Q Γ) (tapes₀ tapes₁ : Fin k.succ → Turing.Tape Γ) :
+  (∀ i, (tm.eval tapes₀).map (fun t => t i) = Part.some (tapes₁ i)) →
+  tm.eval tapes₀ = Part.some tapes₁ := by
+  intro h_eval
+  have h_dom : (tm.eval tapes₀).Dom := by sorry
+  rw [Part.eq_some_iff]
+  use h_dom
+  funext i
+  let x := h_eval i
+  rw [Part.eq_some_iff] at x
+  simp at x
+  simp [h_eval i, h_dom, x]
+  grind
+
 --- Another way to define semantics of a Turing machine: As a relation
 --- between the initial and final tape state.
 def TM.transforms_in_exact_time {k : ℕ} {Q Γ : Type*}

From 574d1945f058356102e2d4255e686325a706f825 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 14:07:29 +0100
Subject: [PATCH 06/21] eval_ext

---
 Complexity/TuringMachine.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Complexity/TuringMachine.lean b/Complexity/TuringMachine.lean
index a700df8..e9e12ed 100644
--- a/Complexity/TuringMachine.lean
+++ b/Complexity/TuringMachine.lean
@@ -77,21 +77,18 @@ def TM.eval {k : ℕ} {Q Γ : Type*}
   (PartENat.find (fun t => (tm.configurations tapes t).state = tm.stopState)).map
     fun t => (tm.configurations tapes t).tapes
 
+--- Extensionality lemma for the tapes of a computation.
 lemma TM.eval_tapes_ext {k : ℕ} {Q Γ : Type*}
   [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q]
   (tm : TM k.succ Q Γ) (tapes₀ tapes₁ : Fin k.succ → Turing.Tape Γ) :
   (∀ i, (tm.eval tapes₀).map (fun t => t i) = Part.some (tapes₁ i)) →
   tm.eval tapes₀ = Part.some tapes₁ := by
   intro h_eval
-  have h_dom : (tm.eval tapes₀).Dom := by sorry
+  have h_dom : (tm.eval tapes₀).Dom := (Part.eq_some_iff.mp (h_eval 0)).1
   rw [Part.eq_some_iff]
   use h_dom
   funext i
-  let x := h_eval i
-  rw [Part.eq_some_iff] at x
-  simp at x
-  simp [h_eval i, h_dom, x]
-  grind
+  simpa [Part.map_get] using (Part.eq_some_iff.mp (h_eval i)).2
 
 --- Another way to define semantics of a Turing machine: As a relation
 --- between the initial and final tape state.

From 28fda537cb465212ad75b34fddb64a25250f41ea Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 16:44:34 +0100
Subject: [PATCH 07/21] eq

---
 Complexity/Eq.lean       | 35 ++++++++++++++++++++++++++++-------
 Complexity/Routines.lean |  4 ++++
 2 files changed, 32 insertions(+), 7 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index ca9d111..26fcd24 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -147,16 +147,37 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
         list_to_tape (w₁ :: ws₁),
         list_to_tape (w₂ :: ws₂),
         .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get) := by
-    -- TODO create a therem that moves the `.get i` into the `Part.some`?
-    simp only [Fin.isValue, TM.with_tapes.eval_1, Nat.succ_eq_add_one, Nat.reduceAdd,
-      Function.comp_apply, List.get_eq_getElem, List.length_cons, List.length_nil,
-      Fin.coe_ofNat_eq_mod, Nat.mod_succ, List.getElem_cons_succ, List.getElem_cons_zero,
-      TM.seq.eval, cons_empty_eval, Part.bind_some, move.eval, Part.map_some, Part.some_inj]
-    funext i
+    apply TM.eval_tapes_ext
+    intro i
     match i with
     | 0 | 1 | 2 =>
+      simp only [TM.with_tapes.eval_1, Function.comp_apply, TM.seq.eval, cons_empty_eval]
       simp [Turing.Tape.mk₁, h_blank_is_default, list_to_tape, Turing.Tape.mk₂]
+  have h_part2_same (w : List Char) :
+    eq_core.eval [
+        list_to_tape (w :: ws₁),
+        list_to_tape (w :: ws₂),
+        .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
+      Part.some [
+        .mk₂ (w.coe_schar.reverse) (.sep :: list_to_string ws₁),
+        .mk₂ (w.coe_schar.reverse) (.sep :: list_to_string ws₂),
+        list_to_tape (['1'] :: ws₃)
+      ].get := by
+    rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
+    rw [eq_core_eval_same [] w.coe_schar
+      (list_to_string ws₁)
+      (list_to_string ws₂)
+      (list_to_string ([] :: ws₃))
+      (by exact List.not_sep_getElem_coe_schar)]
+    simp only [Part.some_inj]
+    rw [List.append_nil, list_to_tape]
+    rw [Turing.Tape.mk₁]
+    have : list_to_string (['1'] :: ws₃) = SChar.ofChar '1' :: list_to_string ([] :: ws₃) := by sorry
+    rw [this]
 
   by_cases h : w₁ = w₂
-  · simp [h]; sorry
+  · subst h
+    apply TM.eval_tapes_ext
+    intro i
+    match i with | 0 | 1 | 2 => simp [h, eq, h_part1, h_part2_same w₁]; sorry
   · simp [h]; sorry
diff --git a/Complexity/Routines.lean b/Complexity/Routines.lean
index 4ccfcd9..a98112c 100644
--- a/Complexity/Routines.lean
+++ b/Complexity/Routines.lean
@@ -45,6 +45,10 @@ lemma List.coe_schar_get_neq_sep (x : List Char) (n : Fin x.coe_schar.length) :
   x.coe_schar.get n ≠ .sep := by
   simp [List.coe_schar]
 
+lemma List.not_sep_getElem_coe_schar {x : List Char} :
+  .sep ∉ x.coe_schar := by
+  simp [List.coe_schar]
+
 lemma List.coe_schar_get_neq_blank (x : List Char) (n : Fin x.coe_schar.length) :
   x.coe_schar.get n ≠ .blank := by
   simp [List.coe_schar]

From 901c50e8c1cbfd35aa2240410a1141f8c047ef99 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 16:51:03 +0100
Subject: [PATCH 08/21] more

---
 Complexity/Eq.lean | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 26fcd24..2a400e1 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -172,12 +172,27 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
     simp only [Part.some_inj]
     rw [List.append_nil, list_to_tape]
     rw [Turing.Tape.mk₁]
-    have : list_to_string (['1'] :: ws₃) = SChar.ofChar '1' :: list_to_string ([] :: ws₃) := by sorry
+    have : list_to_string (['1'] :: ws₃) = .ofChar '1' :: list_to_string ([] :: ws₃) := by
+      simp [list_to_string, List.coe_schar]
     rw [this]
 
+  have h_part2_different (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
+    eq_core.eval [
+        list_to_tape (w₁ :: ws₁),
+        list_to_tape (w₂ :: ws₂),
+        .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
+      Part.some [
+        sorry,  -- First tape after eq_core
+        sorry,  -- Second tape after eq_core
+        list_to_tape ([] :: ws₃)
+      ].get := by
+    rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
+    -- Apply eq_core_eval_different for the case where w₁ and w₂ differ
+    sorry
+
   by_cases h : w₁ = w₂
   · subst h
     apply TM.eval_tapes_ext
     intro i
-    match i with | 0 | 1 | 2 => simp [h, eq, h_part1, h_part2_same w₁]; sorry
+    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2_same w₁]; sorry
   · simp [h]; sorry

From 8daf4d2134e07126a7c3269e3bdd5638a3828b5b Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 16:54:41 +0100
Subject: [PATCH 09/21] more

---
 Complexity/Eq.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 2a400e1..ef0ab05 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -176,14 +176,15 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
       simp [list_to_string, List.coe_schar]
     rw [this]
 
-  have h_part2_different (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
+  have h_part2_different (h_neq : w₁ ≠ w₂) :
+    ∃ n < w₁.length,
     eq_core.eval [
-        list_to_tape (w₁ :: ws₁),
-        list_to_tape (w₂ :: ws₂),
+        (.move .right)^[n] (list_to_tape (w₁ :: ws₁)),
+        (.move .right)^[n] (list_to_tape (w₂ :: ws₂)),
         .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
       Part.some [
-        sorry,  -- First tape after eq_core
-        sorry,  -- Second tape after eq_core
+        .mk₂ (w₁.coe_schar.reverse) (.sep :: list_to_string ws₁),
+        .mk₂ (w₂.coe_schar.reverse) (.sep :: list_to_string ws₂),
         list_to_tape ([] :: ws₃)
       ].get := by
     rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]

From f3a52f2196141770b903f46b75777d58eb3c3c70 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 17:27:53 +0100
Subject: [PATCH 10/21] prog

---
 Complexity/Eq.lean | 81 ++++++++++++++++++++++++----------------------
 1 file changed, 42 insertions(+), 39 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index ef0ab05..b7e351d 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -118,6 +118,43 @@ lemma eq_core_eval_same
   rw [eq_core_steps_equal l r (.sep :: r₁) (.sep :: r₂) r₃ h_r_non_sep]
   rw [eq_core_step_separators (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
 
+lemma eq_core_eval_same_words (w : List Char) (ws₁ ws₂ ws₃ : List (List Char)) :
+  eq_core.eval [
+      list_to_tape (w :: ws₁),
+      list_to_tape (w :: ws₂),
+      .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
+    Part.some [
+      .mk₂ (w.coe_schar.reverse) (.sep :: list_to_string ws₁),
+      .mk₂ (w.coe_schar.reverse) (.sep :: list_to_string ws₂),
+      list_to_tape (['1'] :: ws₃)
+    ].get := by
+  rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
+  rw [eq_core_eval_same [] w.coe_schar
+    (list_to_string ws₁)
+    (list_to_string ws₂)
+    (list_to_string ([] :: ws₃))
+    (by exact List.not_sep_getElem_coe_schar)]
+  simp only [Part.some_inj]
+  rw [List.append_nil, list_to_tape]
+  rw [Turing.Tape.mk₁]
+  have : list_to_string (['1'] :: ws₃) = .ofChar '1' :: list_to_string ([] :: ws₃) := by
+    simp [list_to_string, List.coe_schar]
+  rw [this]
+
+lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char))
+    (h_neq : w₁ ≠ w₂) :
+  ∃ n < w₁.length,
+  eq_core.eval [
+      (.move .right)^[n] (list_to_tape (w₁ :: ws₁)),
+      (.move .right)^[n] (list_to_tape (w₂ :: ws₂)),
+      .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
+    Part.some [
+      .mk₂ (w₁.coe_schar.reverse) (.sep :: list_to_string ws₁),
+      .mk₂ (w₂.coe_schar.reverse) (.sep :: list_to_string ws₂),
+      list_to_tape ([] :: ws₃)
+    ].get := by
+  sorry
+
 --- A 3-tape Turing machine that pushes the new word "1"
 --- to the third tape if the first words on the first tape are the same
 --- and otherwise pushes the empty word to the third tape.
@@ -133,6 +170,7 @@ def Routines.eq :=
   (Routines.move_to_start.with_tapes #v[0])).seq
   (Routines.move_to_start.with_tapes #v[1])
 
+
 @[simp]
 theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char)) :
   Routines.eq.eval (list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ws₃].get) =
@@ -153,47 +191,12 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
     | 0 | 1 | 2 =>
       simp only [TM.with_tapes.eval_1, Function.comp_apply, TM.seq.eval, cons_empty_eval]
       simp [Turing.Tape.mk₁, h_blank_is_default, list_to_tape, Turing.Tape.mk₂]
-  have h_part2_same (w : List Char) :
-    eq_core.eval [
-        list_to_tape (w :: ws₁),
-        list_to_tape (w :: ws₂),
-        .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
-      Part.some [
-        .mk₂ (w.coe_schar.reverse) (.sep :: list_to_string ws₁),
-        .mk₂ (w.coe_schar.reverse) (.sep :: list_to_string ws₂),
-        list_to_tape (['1'] :: ws₃)
-      ].get := by
-    rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
-    rw [eq_core_eval_same [] w.coe_schar
-      (list_to_string ws₁)
-      (list_to_string ws₂)
-      (list_to_string ([] :: ws₃))
-      (by exact List.not_sep_getElem_coe_schar)]
-    simp only [Part.some_inj]
-    rw [List.append_nil, list_to_tape]
-    rw [Turing.Tape.mk₁]
-    have : list_to_string (['1'] :: ws₃) = .ofChar '1' :: list_to_string ([] :: ws₃) := by
-      simp [list_to_string, List.coe_schar]
-    rw [this]
-
-  have h_part2_different (h_neq : w₁ ≠ w₂) :
-    ∃ n < w₁.length,
-    eq_core.eval [
-        (.move .right)^[n] (list_to_tape (w₁ :: ws₁)),
-        (.move .right)^[n] (list_to_tape (w₂ :: ws₂)),
-        .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
-      Part.some [
-        .mk₂ (w₁.coe_schar.reverse) (.sep :: list_to_string ws₁),
-        .mk₂ (w₂.coe_schar.reverse) (.sep :: list_to_string ws₂),
-        list_to_tape ([] :: ws₃)
-      ].get := by
-    rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
-    -- Apply eq_core_eval_different for the case where w₁ and w₂ differ
-    sorry
 
   by_cases h : w₁ = w₂
   · subst h
+    have h_part2 := eq_core_eval_same_words w₁ ws₁ ws₂ ws₃
     apply TM.eval_tapes_ext
     intro i
-    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2_same w₁]; sorry
-  · simp [h]; sorry
+    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2]; sorry
+  · have h_part2 := eq_core_eval_different_words w₁ w₂ ws₁ ws₂ ws₃ h
+    simp [h]; sorry

From 0115bd26eb330d8e1a34d57765ed5dcaf38f2d65 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 17:30:34 +0100
Subject: [PATCH 11/21] prog

---
 Complexity/Eq.lean | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index b7e351d..d1f2d51 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -87,22 +87,6 @@ lemma eq_core_steps_equal
     funext
     simp
 
-lemma eq_core_eval_different
-  (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
-  (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
-  eq_core.eval [.mk₂ l (r ++ (a :: r₁)), .mk₂ l (r ++ (b :: r₂)), .mk₂ [] (.blank :: r₃)].get =
-    Part.some [
-      .mk₂ (r.reverse ++ l) (a :: r₁),
-      .mk₂ (r.reverse ++ l) (b :: r₂),
-      .mk₂ [] r₃].get := by
-  have h_start_state : eq_core.startState = 0 := rfl
-  apply TM.eval_of_transforms
-  apply TM.transforms_of_inert _ _ _ eq_core.is_inert_after_stop
-  use r.length.succ
-  simp only [TM.configurations, Function.iterate_succ_apply']
-  rw [eq_core_steps_equal l r (a :: r₁) (b :: r₂) r₃ h_r_non_sep]
-  rw [eq_core_step_non_equal a b h_neq₁ h_neq₂ h_neq₃ (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
-
 lemma eq_core_eval_same
   (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
   eq_core.eval [.mk₂ l (r ++ .sep :: r₁), .mk₂ l (r ++ .sep :: r₂), .mk₂ [] (.blank :: r₃)].get =
@@ -141,16 +125,32 @@ lemma eq_core_eval_same_words (w : List Char) (ws₁ ws₂ ws₃ : List (List Ch
     simp [list_to_string, List.coe_schar]
   rw [this]
 
+lemma eq_core_eval_different
+  (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
+  (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
+  eq_core.eval [.mk₂ l (r ++ (a :: r₁)), .mk₂ l (r ++ (b :: r₂)), .mk₂ [] (.blank :: r₃)].get =
+    Part.some [
+      .mk₂ (r.reverse ++ l) (a :: r₁),
+      .mk₂ (r.reverse ++ l) (b :: r₂),
+      .mk₂ [] r₃].get := by
+  have h_start_state : eq_core.startState = 0 := rfl
+  apply TM.eval_of_transforms
+  apply TM.transforms_of_inert _ _ _ eq_core.is_inert_after_stop
+  use r.length.succ
+  simp only [TM.configurations, Function.iterate_succ_apply']
+  rw [eq_core_steps_equal l r (a :: r₁) (b :: r₂) r₃ h_r_non_sep]
+  rw [eq_core_step_non_equal a b h_neq₁ h_neq₂ h_neq₃ (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
+
 lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char))
     (h_neq : w₁ ≠ w₂) :
-  ∃ n < w₁.length,
+  ∃ n ≤ min w₁.length w₂.length,
   eq_core.eval [
-      (.move .right)^[n] (list_to_tape (w₁ :: ws₁)),
-      (.move .right)^[n] (list_to_tape (w₂ :: ws₂)),
+      list_to_tape (w₁ :: ws₁),
+      list_to_tape (w₂ :: ws₂),
       .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
     Part.some [
-      .mk₂ (w₁.coe_schar.reverse) (.sep :: list_to_string ws₁),
-      .mk₂ (w₂.coe_schar.reverse) (.sep :: list_to_string ws₂),
+      (.move .right)^[n] (list_to_tape (w₁ :: ws₁)),
+      (.move .right)^[n] (list_to_tape (w₂ :: ws₂)),
       list_to_tape ([] :: ws₃)
     ].get := by
   sorry

From 1c247a125e491f1abec1293e67761fe963cdf4f4 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 18:17:03 +0100
Subject: [PATCH 12/21] differ

---
 Complexity/Eq.lean | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index d1f2d51..7e54ea2 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -141,6 +141,16 @@ lemma eq_core_eval_different
   rw [eq_core_steps_equal l r (a :: r₁) (b :: r₂) r₃ h_r_non_sep]
   rw [eq_core_step_non_equal a b h_neq₁ h_neq₂ h_neq₃ (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
 
+-- Helper: Find where two different Char lists first differ when encoded as SChar
+-- This gives us the common prefix and first differing characters
+lemma List.coe_schar_differ_at (w1 w2 : List Char) (h_neq : w1 ≠ w2) :
+  ∃ (common rest1 rest2 : List SChar), ∃ (a b : SChar),
+    (∀ c ∈ common, c ≠ .sep) ∧
+    (a ≠ b) ∧
+    w1.coe_schar ++ [SChar.sep] = common ++ a :: rest1 ∧
+    w2.coe_schar ++ [SChar.sep] = common ++ b :: rest2 := by
+  sorry
+
 lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char))
     (h_neq : w₁ ≠ w₂) :
   ∃ n ≤ min w₁.length w₂.length,
@@ -153,6 +163,27 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
       (.move .right)^[n] (list_to_tape (w₂ :: ws₂)),
       list_to_tape ([] :: ws₃)
     ].get := by
+  -- Convert to tape representation
+  rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
+
+  -- Get the decomposition of where the words differ
+  obtain ⟨common, rest1, rest2, h_w1, h_w2, h_common_no_sep, h_differ⟩ :=
+    List.coe_schar_differ_at w₁ w₂ h_neq
+
+  -- Use the length of the common prefix
+  use common.length
+  constructor
+  · -- Show common.length ≤ min w₁.length w₂.length
+    sorry
+
+  -- Now we need to show the evaluation gives the correct result
+  -- Use Tape.move_right_append to move to the position where they differ
+  rw [h_w1, h_w2]
+
+  -- After moving right common.length times, we're at the differing position
+  rw [Tape.move_right_append, Tape.move_right_append]
+
+  -- Now apply eq_core_eval_different or handle the cases
   sorry
 
 --- A 3-tape Turing machine that pushes the new word "1"

From 6ddc64fe1969ecceee9103534779b3d830f60a88 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 18:26:41 +0100
Subject: [PATCH 13/21] differ

---
 Complexity/Eq.lean | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 7e54ea2..13b2ba3 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -143,13 +143,23 @@ lemma eq_core_eval_different
 
 -- Helper: Find where two different Char lists first differ when encoded as SChar
 -- This gives us the common prefix and first differing characters
-lemma List.coe_schar_differ_at (w1 w2 : List Char) (h_neq : w1 ≠ w2) :
+lemma List.coe_schar_differ_at (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
   ∃ (common rest1 rest2 : List SChar), ∃ (a b : SChar),
     (∀ c ∈ common, c ≠ .sep) ∧
     (a ≠ b) ∧
-    w1.coe_schar ++ [SChar.sep] = common ++ a :: rest1 ∧
-    w2.coe_schar ++ [SChar.sep] = common ++ b :: rest2 := by
-  sorry
+    w₁.coe_schar ++ [SChar.sep] = common ++ a :: rest1 ∧
+    w₂.coe_schar ++ [SChar.sep] = common ++ b :: rest2 := by
+  induction w₁ generalizing w₂ with
+  | nil =>
+    -- In this case, common = [], rest1 = [], a = .sep
+    -- and w₂ must be non-empty (because of h_neq). This,
+    -- there is a b such that w₂ = b :: rest2
+    -- we use this b and rest2 for the existentially quantified variables.
+    -- (potentially converted from Char to SChar)
+    -- Then a ≠ b because b is not .sep (it is a charactor of w₂ and List.not_sep_getElem_coe_schar
+    -- ensures that it is not .sep. The other properties should follow by simp.
+    sorry
+  | cons w w₁ ih => sorry
 
 lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char))
     (h_neq : w₁ ≠ w₂) :
@@ -167,7 +177,7 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
   rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
 
   -- Get the decomposition of where the words differ
-  obtain ⟨common, rest1, rest2, h_w1, h_w2, h_common_no_sep, h_differ⟩ :=
+  obtain ⟨common, rest1, rest2, a, b, h_common_no_sep, h_ab_neq, h_w1, h_w2⟩ :=
     List.coe_schar_differ_at w₁ w₂ h_neq
 
   -- Use the length of the common prefix

From ef75d578e6f229b169e97294dc91bae4fbb972a5 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 18:44:52 +0100
Subject: [PATCH 14/21] differ

---
 Complexity/Eq.lean | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 13b2ba3..e82b993 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -149,17 +149,25 @@ lemma List.coe_schar_differ_at (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
     (a ≠ b) ∧
     w₁.coe_schar ++ [SChar.sep] = common ++ a :: rest1 ∧
     w₂.coe_schar ++ [SChar.sep] = common ++ b :: rest2 := by
+  wlog h_length: w₁.length ≤ w₂.length
+  · sorry
   induction w₁ generalizing w₂ with
   | nil =>
-    -- In this case, common = [], rest1 = [], a = .sep
-    -- and w₂ must be non-empty (because of h_neq). This,
-    -- there is a b such that w₂ = b :: rest2
-    -- we use this b and rest2 for the existentially quantified variables.
-    -- (potentially converted from Char to SChar)
-    -- Then a ≠ b because b is not .sep (it is a charactor of w₂ and List.not_sep_getElem_coe_schar
-    -- ensures that it is not .sep. The other properties should follow by simp.
-    sorry
-  | cons w w₁ ih => sorry
+    cases w₂ with
+    | nil => simp at h_neq
+    | cons c w₂' =>
+      use [], [], w₂'.coe_schar ++ [.sep], .sep, .ofChar c
+      simp [List.coe_schar]
+  | cons c w₁ ih =>
+    cases w₂ with
+    | nil => sorry -- contradiction with h_length
+    | cons d w₂' =>
+      by_cases h_char_eq : c = d
+      · -- use induction on w₁ and w₂, then prepend c before common and we should have our result.
+        sorry
+      · -- in this case, common is empty, a = c, b = d and in general, it should be similar to the case
+        -- for nil / cons
+        sorry
 
 lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char))
     (h_neq : w₁ ≠ w₂) :

From a9ef7c616ab6168673e12d827a37c9ac5eb10de6 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 19:02:02 +0100
Subject: [PATCH 15/21] differ

---
 Complexity/Eq.lean | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index e82b993..de7cf6e 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -150,7 +150,12 @@ lemma List.coe_schar_differ_at (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
     w₁.coe_schar ++ [SChar.sep] = common ++ a :: rest1 ∧
     w₂.coe_schar ++ [SChar.sep] = common ++ b :: rest2 := by
   wlog h_length: w₁.length ≤ w₂.length
-  · sorry
+  · -- Symmetric case: if w₂.length ≤ w₁.length, swap them
+    have h_w2_le : w₂.length ≤ w₁.length := Nat.le_of_not_le h_length
+    obtain ⟨common, rest2, rest1, b, a, h_no_sep, h_ba_neq, h_w2, h_w1⟩ :=
+      this w₂ w₁ (Ne.symm h_neq) h_w2_le
+    use common, rest1, rest2, a, b
+    exact ⟨h_no_sep, Ne.symm h_ba_neq, h_w1, h_w2⟩
   induction w₁ generalizing w₂ with
   | nil =>
     cases w₂ with
@@ -160,14 +165,31 @@ lemma List.coe_schar_differ_at (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
       simp [List.coe_schar]
   | cons c w₁ ih =>
     cases w₂ with
-    | nil => sorry -- contradiction with h_length
+    | nil =>
+      -- contradiction with h_length: (c :: w₁).length ≤ [].length is false
+      simp at h_length
     | cons d w₂' =>
       by_cases h_char_eq : c = d
-      · -- use induction on w₁ and w₂, then prepend c before common and we should have our result.
-        sorry
-      · -- in this case, common is empty, a = c, b = d and in general, it should be similar to the case
-        -- for nil / cons
-        sorry
+      · -- Characters equal, use induction on tails
+        subst h_char_eq
+        obtain ⟨common, rest1, rest2, a, b, h_no_sep, h_ab_neq, h_w1', h_w2'⟩ :=
+          ih w₂' (by simpa using h_neq) (by simp at h_length; omega)
+        use .ofChar c :: common, rest1, rest2, a, b
+        simp only [List.coe_schar, List.map_cons, List.cons_append]
+        constructor
+        · -- Show ∀ x ∈ .ofChar c :: common, x ≠ .sep
+          intro x h_mem
+          cases h_mem with
+          | head => simp
+          | tail _ h => exact h_no_sep x h
+        · constructor
+          · exact h_ab_neq
+          · constructor
+            · simpa [List.coe_schar] using h_w1'
+            · simpa [List.coe_schar] using h_w2'
+      · -- Characters differ: common is empty
+        use [], w₁.coe_schar ++ [.sep], w₂'.coe_schar ++ [.sep], .ofChar c, .ofChar d
+        simp [List.coe_schar, h_char_eq]
 
 lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char))
     (h_neq : w₁ ≠ w₂) :

From 7b9e7a8d4d1a208d5af22fa81d257a5b70670527 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 19:41:20 +0100
Subject: [PATCH 16/21] differ

---
 Complexity/Eq.lean | 75 +++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 65 insertions(+), 10 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index de7cf6e..337fcf5 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -54,20 +54,20 @@ lemma eq_core_step_equal (a : SChar) (h_neq : a ≠ .sep) (l₁ l₂ r₁ r₂ r
       simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
 
 lemma eq_core_step_non_equal
-  (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
+  (a b : SChar) (h_neq₁ : a ≠ b)
   (l₁ l₂ r₁ r₂ r₃ : List SChar) :
   eq_core.transition.step
     ⟨eq_core.startState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₂ [] (.blank :: r₃)].get⟩ =
     ⟨eq_core.stopState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₂ [] r₃].get⟩ := by
   have h_blank_default : SChar.blank = default := rfl
+  have h_neq_seq : ¬(a = .sep ∧ b = .sep) := by grind
   ext1
-  · simp [h_neq₁, h_neq₂, h_neq₃, eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
+  · simp_all [eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
   · dsimp
     funext i
     match i with
     | 0 | 1 | 2 =>
-      simp [h_blank_default, h_neq₁, h_neq₂, h_neq₃, eq_core,
-            Transition.step, Turing.Tape.mk₂, performTapeOps]
+      simp_all [eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
 
 lemma eq_core_steps_equal
   (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
@@ -213,18 +213,73 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
   -- Use the length of the common prefix
   use common.length
   constructor
-  · -- Show common.length ≤ min w₁.length w₂.length
-    sorry
+  · have h1 : common.length ≤ w₁.length := by
+      have : (w₁.coe_schar ++ [SChar.sep]).length = (common ++ a :: rest1).length :=
+        congrArg List.length h_w1
+      simp at this
+      have : w₁.coe_schar.length = w₁.length := List.coe_schar_length w₁
+      omega
+    have h2 : common.length ≤ w₂.length := by
+      have : (w₂.coe_schar ++ [SChar.sep]).length = (common ++ b :: rest2).length :=
+        congrArg List.length h_w2
+      simp at this
+      have : w₂.coe_schar.length = w₂.length := List.coe_schar_length w₂
+      omega
+    omega
 
   -- Now we need to show the evaluation gives the correct result
-  -- Use Tape.move_right_append to move to the position where they differ
-  rw [h_w1, h_w2]
+  -- Rewrite using the decompositions
+  have h_w1_eq : w₁.coe_schar ++ SChar.sep :: list_to_string ws₁ =
+                  common ++ a :: (rest1 ++ list_to_string ws₁) := by
+    calc w₁.coe_schar ++ SChar.sep :: list_to_string ws₁
+        = w₁.coe_schar ++ [SChar.sep] ++ list_to_string ws₁ := by simp
+      _ = common ++ a :: (rest1 ++ list_to_string ws₁) := by simp [h_w1]
+  have h_w2_eq : w₂.coe_schar ++ SChar.sep :: list_to_string ws₂ =
+                  common ++ b :: (rest2 ++ list_to_string ws₂) := by
+    calc w₂.coe_schar ++ SChar.sep :: list_to_string ws₂
+        = w₂.coe_schar ++ [SChar.sep] ++ list_to_string ws₂ := by simp
+      _ = common ++ b :: (rest2 ++ list_to_string ws₂) := by simp [h_w2]
+
+  rw [h_w1_eq, h_w2_eq]
 
   -- After moving right common.length times, we're at the differing position
   rw [Tape.move_right_append, Tape.move_right_append]
 
-  -- Now apply eq_core_eval_different or handle the cases
-  sorry
+  -- Now we have tapes positioned at the differing characters a and b
+  -- We need to show neither a nor b is .sep
+  -- Since a ≠ b and they're the first differing characters, at most one can be .sep
+  -- But actually, both must be from the words (not the appended separator)
+  -- because common contains the longest prefix where they match
+  have h_a_not_sep : a ≠ SChar.sep := by
+    -- If a = .sep, then from h_w1, we have common = w₁.coe_schar and rest1 = []
+    -- But w₁.coe_schar has no separators, so this would mean common has length w₁.length
+    -- Similarly for h_w2 with b
+    -- Since a ≠ b, if a = .sep then b ≠ .sep
+    -- But then w₂.coe_schar = common ++ b :: rest2 where b is not sep
+    -- This means common.length < w₂.coe_schar.length
+    -- Combined with common = w₁.coe_schar, we'd have w₁.length < w₂.length
+    -- and w₂[w₁.length] = b ≠ .sep, which is fine
+    -- But we also have w₁.coe_schar has no .sep, contradicting a = .sep coming after common
+    sorry
+  have h_b_not_sep : b ≠ SChar.sep := by
+    -- Symmetric argument
+    sorry
+
+  -- Convert the no-sep hypothesis to the form needed by eq_core_eval_different
+  have h_common_no_sep' : .sep ∉ common := by
+    intro h_mem
+    exact h_common_no_sep .sep h_mem rfl
+
+  -- Apply eq_core_eval_different
+  -- We have: mk₂ (common.reverse ++ []) (a :: rest1 ++ ...)
+  -- This matches eq_core_eval_different with l=[], r=common
+  convert eq_core_eval_different a b h_ab_neq h_a_not_sep h_b_not_sep
+    [] common
+    (rest1 ++ list_to_string ws₁)
+    (rest2 ++ list_to_string ws₂)
+    (list_to_string ([] :: ws₃))
+    h_common_no_sep' using 2
+  all_goals simp [list_to_tape]
 
 --- A 3-tape Turing machine that pushes the new word "1"
 --- to the third tape if the first words on the first tape are the same

From 72d07586fdfdee3e5e35eccc04f6479cfed96965 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 19:42:56 +0100
Subject: [PATCH 17/21] differ

---
 Complexity/Eq.lean | 43 +++++--------------------------------------
 1 file changed, 5 insertions(+), 38 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 337fcf5..8ff7f99 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -54,8 +54,7 @@ lemma eq_core_step_equal (a : SChar) (h_neq : a ≠ .sep) (l₁ l₂ r₁ r₂ r
       simp [h_neq, eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
 
 lemma eq_core_step_non_equal
-  (a b : SChar) (h_neq₁ : a ≠ b)
-  (l₁ l₂ r₁ r₂ r₃ : List SChar) :
+  (a b : SChar) (h_neq₁ : a ≠ b) (l₁ l₂ r₁ r₂ r₃ : List SChar) :
   eq_core.transition.step
     ⟨eq_core.startState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₂ [] (.blank :: r₃)].get⟩ =
     ⟨eq_core.stopState, [.mk₂ l₁ (a :: r₁), .mk₂ l₂ (b :: r₂), .mk₂ [] r₃].get⟩ := by
@@ -126,7 +125,7 @@ lemma eq_core_eval_same_words (w : List Char) (ws₁ ws₂ ws₃ : List (List Ch
   rw [this]
 
 lemma eq_core_eval_different
-  (a b : SChar) (h_neq₁ : a ≠ b) (h_neq₂ : a ≠ .sep) (h_neq₃ : b ≠ .sep)
+  (a b : SChar) (h_neq₁ : a ≠ b)
   (l r r₁ r₂ r₃ : List SChar) (h_r_non_sep : .sep ∉ r) :
   eq_core.eval [.mk₂ l (r ++ (a :: r₁)), .mk₂ l (r ++ (b :: r₂)), .mk₂ [] (.blank :: r₃)].get =
     Part.some [
@@ -139,7 +138,7 @@ lemma eq_core_eval_different
   use r.length.succ
   simp only [TM.configurations, Function.iterate_succ_apply']
   rw [eq_core_steps_equal l r (a :: r₁) (b :: r₂) r₃ h_r_non_sep]
-  rw [eq_core_step_non_equal a b h_neq₁ h_neq₂ h_neq₃ (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
+  rw [eq_core_step_non_equal a b h_neq₁ (r.reverse ++ l) (r.reverse ++ l) r₁ r₂ r₃]
 
 -- Helper: Find where two different Char lists first differ when encoded as SChar
 -- This gives us the common prefix and first differing characters
@@ -205,11 +204,9 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
     ].get := by
   -- Convert to tape representation
   rw [list_to_tape_cons, list_to_tape_cons, Turing.Tape.mk₁, Turing.Tape.mk₁]
-
   -- Get the decomposition of where the words differ
   obtain ⟨common, rest1, rest2, a, b, h_common_no_sep, h_ab_neq, h_w1, h_w2⟩ :=
     List.coe_schar_differ_at w₁ w₂ h_neq
-
   -- Use the length of the common prefix
   use common.length
   constructor
@@ -226,7 +223,6 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
       have : w₂.coe_schar.length = w₂.length := List.coe_schar_length w₂
       omega
     omega
-
   -- Now we need to show the evaluation gives the correct result
   -- Rewrite using the decompositions
   have h_w1_eq : w₁.coe_schar ++ SChar.sep :: list_to_string ws₁ =
@@ -239,47 +235,18 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
     calc w₂.coe_schar ++ SChar.sep :: list_to_string ws₂
         = w₂.coe_schar ++ [SChar.sep] ++ list_to_string ws₂ := by simp
       _ = common ++ b :: (rest2 ++ list_to_string ws₂) := by simp [h_w2]
-
   rw [h_w1_eq, h_w2_eq]
-
-  -- After moving right common.length times, we're at the differing position
   rw [Tape.move_right_append, Tape.move_right_append]
-
-  -- Now we have tapes positioned at the differing characters a and b
-  -- We need to show neither a nor b is .sep
-  -- Since a ≠ b and they're the first differing characters, at most one can be .sep
-  -- But actually, both must be from the words (not the appended separator)
-  -- because common contains the longest prefix where they match
-  have h_a_not_sep : a ≠ SChar.sep := by
-    -- If a = .sep, then from h_w1, we have common = w₁.coe_schar and rest1 = []
-    -- But w₁.coe_schar has no separators, so this would mean common has length w₁.length
-    -- Similarly for h_w2 with b
-    -- Since a ≠ b, if a = .sep then b ≠ .sep
-    -- But then w₂.coe_schar = common ++ b :: rest2 where b is not sep
-    -- This means common.length < w₂.coe_schar.length
-    -- Combined with common = w₁.coe_schar, we'd have w₁.length < w₂.length
-    -- and w₂[w₁.length] = b ≠ .sep, which is fine
-    -- But we also have w₁.coe_schar has no .sep, contradicting a = .sep coming after common
-    sorry
-  have h_b_not_sep : b ≠ SChar.sep := by
-    -- Symmetric argument
-    sorry
-
-  -- Convert the no-sep hypothesis to the form needed by eq_core_eval_different
   have h_common_no_sep' : .sep ∉ common := by
     intro h_mem
     exact h_common_no_sep .sep h_mem rfl
-
-  -- Apply eq_core_eval_different
-  -- We have: mk₂ (common.reverse ++ []) (a :: rest1 ++ ...)
-  -- This matches eq_core_eval_different with l=[], r=common
-  convert eq_core_eval_different a b h_ab_neq h_a_not_sep h_b_not_sep
+  convert eq_core_eval_different a b h_ab_neq
     [] common
     (rest1 ++ list_to_string ws₁)
     (rest2 ++ list_to_string ws₂)
     (list_to_string ([] :: ws₃))
     h_common_no_sep' using 2
-  all_goals simp [list_to_tape]
+
 
 --- A 3-tape Turing machine that pushes the new word "1"
 --- to the third tape if the first words on the first tape are the same

From a566d507b1daa9123efd9b8b47d04337de5a5880 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 20:11:58 +0100
Subject: [PATCH 18/21] eq

---
 Complexity/Eq.lean | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index 8ff7f99..e499d9b 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -214,13 +214,11 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
       have : (w₁.coe_schar ++ [SChar.sep]).length = (common ++ a :: rest1).length :=
         congrArg List.length h_w1
       simp at this
-      have : w₁.coe_schar.length = w₁.length := List.coe_schar_length w₁
       omega
     have h2 : common.length ≤ w₂.length := by
       have : (w₂.coe_schar ++ [SChar.sep]).length = (common ++ b :: rest2).length :=
         congrArg List.length h_w2
       simp at this
-      have : w₂.coe_schar.length = w₂.length := List.coe_schar_length w₂
       omega
     omega
   -- Now we need to show the evaluation gives the correct result
@@ -251,19 +249,12 @@ lemma eq_core_eval_different_words (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ :
 --- A 3-tape Turing machine that pushes the new word "1"
 --- to the third tape if the first words on the first tape are the same
 --- and otherwise pushes the empty word to the third tape.
-
--- push empty word on the third tape
--- move left on the third tape
--- run core
--- run "move_to_start" on first tape
--- run "move_to_start" on second tape
 def Routines.eq :=
   (((((cons_empty.seq (Routines.move .left)).with_tapes #v[2]) : TM 3 _ _).seq
     eq_core).seq
   (Routines.move_to_start.with_tapes #v[0])).seq
   (Routines.move_to_start.with_tapes #v[1])
 
-
 @[simp]
 theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char)) :
   Routines.eq.eval (list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ws₃].get) =
@@ -291,5 +282,7 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
     apply TM.eval_tapes_ext
     intro i
     match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2]; sorry
-  · have h_part2 := eq_core_eval_different_words w₁ w₂ ws₁ ws₂ ws₃ h
-    simp [h]; sorry
+  · obtain ⟨n, h_n_le, h_part2⟩ := eq_core_eval_different_words w₁ w₂ ws₁ ws₂ ws₃ h
+    apply TM.eval_tapes_ext
+    intro i
+    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2]; sorry

From 06faf56a2fb7cb2594c83e0bae67468132cfb3b1 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 27 Jan 2026 22:40:22 +0100
Subject: [PATCH 19/21] eq

---
 Complexity/Eq.lean | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index e499d9b..f0297d3 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -275,14 +275,18 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
     | 0 | 1 | 2 =>
       simp only [TM.with_tapes.eval_1, Function.comp_apply, TM.seq.eval, cons_empty_eval]
       simp [Turing.Tape.mk₁, h_blank_is_default, list_to_tape, Turing.Tape.mk₂]
-
   by_cases h : w₁ = w₂
   · subst h
     have h_part2 := eq_core_eval_same_words w₁ ws₁ ws₂ ws₃
     apply TM.eval_tapes_ext
+    let h_move := fun r => move_to_start_eval (r := r) (c := .sep)
+      (l := w₁.coe_schar.reverse) (by decide) (by simp [List.coe_schar])
+    have h_list_to_tape {rest : List (List Char)} :
+      Turing.Tape.mk₂ [] (w₁.coe_schar ++ SChar.sep :: list_to_string rest) =
+      list_to_tape (w₁ :: rest) := by simp [list_to_tape, Turing.Tape.mk₁]
     intro i
-    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2]; sorry
+    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2, h_move, h_list_to_tape]
   · obtain ⟨n, h_n_le, h_part2⟩ := eq_core_eval_different_words w₁ w₂ ws₁ ws₂ ws₃ h
     apply TM.eval_tapes_ext
     intro i
-    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2]; sorry
+    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2];  sorry

From 64fdba4c934fbd4802f030096bb94210fb51864d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 28 Jan 2026 10:56:51 +0100
Subject: [PATCH 20/21] another form of the move until eval

---
 Complexity/Eq.lean        |  9 ++++++-
 Complexity/MoveUntil.lean | 54 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+), 1 deletion(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index f0297d3..e586f02 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -288,5 +288,12 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
     match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2, h_move, h_list_to_tape]
   · obtain ⟨n, h_n_le, h_part2⟩ := eq_core_eval_different_words w₁ w₂ ws₁ ws₂ ws₃ h
     apply TM.eval_tapes_ext
+    have h_move :
+      (move_to_start.eval
+      fun x => (.move .right)^[n] (list_to_tape (w₁ :: ws₁))) =
+      sorry := by sorry
     intro i
-    match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2];  sorry
+    match i with
+    | 0 => simp [eq, h_part1, h_part2];  sorry
+    | 1 => simp [eq, h_part1, h_part2];  sorry
+    | 2 => simp [eq, h_part1, h_part2];  sorry
diff --git a/Complexity/MoveUntil.lean b/Complexity/MoveUntil.lean
index 3c785cf..b0a3b45 100644
--- a/Complexity/MoveUntil.lean
+++ b/Complexity/MoveUntil.lean
@@ -185,3 +185,57 @@ theorem Routines.move_to_start_eval
       · grind
   · convert Routines.move.semantics (dir := .right) (Γ := SChar)
     simp [Turing.Tape.mk₁]
+
+@[simp]
+theorem Routines.move_to_start_eval'
+  {w : List SChar} {n : ℕ}
+  (h_n_le : n < w.length)
+  (h_non_blank : ∀ i, ∀ h : i ≤ n, w[i]'(Nat.lt_of_le_of_lt h h_n_le) ≠ .blank) :
+  Routines.move_to_start.eval (fun _ => (.move .right)^[n] (.mk₂ [] w)) =
+    Part.some (fun _ => .mk₂ [] w) := by
+  -- Split w into prefix and suffix
+  let w₁ := w.take n
+  let w₂ := w.drop n
+  have h_w_eq : w = w₁ ++ w₂ := by simp [w₁, w₂]
+  have h_w₁_length : w₁.length = n := by simp [w₁, List.length_take]; omega
+  have h_w₂_nonempty : w₂ ≠ [] := by
+    simp [w₂, List.drop_eq_nil_iff]
+    omega
+  -- Get the head of w₂
+  obtain ⟨c, w'₂, h_w₂_eq⟩ := List.exists_cons_of_ne_nil h_w₂_nonempty
+  -- Prove c ≠ blank
+  have h_c_non_blank : c ≠ .blank := by
+    have h1 : c = w₂.head h_w₂_nonempty := by simp [h_w₂_eq]
+    have h2 : w₂.head h_w₂_nonempty = w[n] := by
+      simp [w₂, List.head_drop]
+    rw [h1, h2]
+    exact h_non_blank n (by omega)
+  -- Prove blank ∉ w₁
+  have h_w₁_non_blank : .blank ∉ w₁ := by
+    intro h_contra
+    have h_mem : ∃ (i : Fin w₁.length), w₁[i] = .blank := by
+      simp only [List.mem_iff_get] at h_contra
+      exact h_contra
+    rcases h_mem with ⟨i, h_i_eq⟩
+    have h_i_lt_n : i.val < n := by
+      simp [w₁, List.length_take] at i
+      omega
+    have h_eq : w₁[i] = w[i.val] := by
+      simp [w₁, List.getElem_take]
+    rw [h_eq] at h_i_eq
+    have h_neq : w[i.val] ≠ .blank := h_non_blank i.val (by omega)
+    exact h_neq h_i_eq
+  -- Prove blank ∉ w₁.reverse
+  have h_w₁_rev_non_blank : .blank ∉ w₁.reverse := by
+    simpa [List.mem_reverse] using h_w₁_non_blank
+  -- Rewrite using the split and apply Tape.move_right_append
+  rw [h_w_eq, h_w₂_eq]
+  have h_tape_eq : (Turing.Tape.move .right)^[n] (Turing.Tape.mk₂ [] (w₁ ++ (c :: w'₂))) =
+                    Turing.Tape.mk₂ (w₁.reverse ++ []) (c :: w'₂) := by
+    rw [← h_w₁_length]
+    exact Tape.move_right_append [] w₁ (c :: w'₂)
+  simp only [List.append_nil] at h_tape_eq
+  rw [h_tape_eq]
+  -- Now apply move_to_start_eval with l := w₁.reverse, r := w'₂
+  have h_eval := @move_to_start_eval c w₁.reverse w'₂ h_c_non_blank h_w₁_rev_non_blank
+  simpa using h_eval

From 282b5098167ee17bfe0dea9355be8c817d0ae3f3 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 28 Jan 2026 18:50:10 +0100
Subject: [PATCH 21/21] eq_eval

---
 Complexity/Eq.lean       | 30 ++++++++++++++++++++++--------
 Complexity/Routines.lean |  4 ++++
 2 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/Complexity/Eq.lean b/Complexity/Eq.lean
index e586f02..642bf7d 100644
--- a/Complexity/Eq.lean
+++ b/Complexity/Eq.lean
@@ -258,7 +258,7 @@ def Routines.eq :=
 @[simp]
 theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List Char)) :
   Routines.eq.eval (list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ws₃].get) =
-    Part.some (if h: w₁ = w₂ then
+    Part.some (if w₁ = w₂ then
       list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, ['1'] :: ws₃].get
     else
       list_to_tape ∘ [w₁ :: ws₁, w₂ :: ws₂, [] :: ws₃].get) := by
@@ -288,12 +288,26 @@ theorem Routines.eq_eval (w₁ w₂ : List Char) (ws₁ ws₂ ws₃ : List (List
     match i with | 0 | 1 | 2 => simp [eq, h_part1, h_part2, h_move, h_list_to_tape]
   · obtain ⟨n, h_n_le, h_part2⟩ := eq_core_eval_different_words w₁ w₂ ws₁ ws₂ ws₃ h
     apply TM.eval_tapes_ext
-    have h_move :
-      (move_to_start.eval
-      fun x => (.move .right)^[n] (list_to_tape (w₁ :: ws₁))) =
-      sorry := by sorry
+    have h_move_w₁ :
+      (move_to_start.eval fun _ => (.move .right)^[n] (list_to_tape (w₁ :: ws₁))) =
+        Part.some fun _ => list_to_tape (w₁ :: ws₁) := by
+      apply Routines.move_to_start_eval'
+      · intro i hi
+        by_contra h_exists_blank
+        let h_has_blank := List.mem_of_getElem h_exists_blank
+        let h_not_has_blank := blank_not_elem_list_to_string (ls := w₁ :: ws₁)
+        contradiction
+      · simp [list_to_string_cons]; omega
+    have h_move_w₂ :
+      (move_to_start.eval fun _ => (.move .right)^[n] (list_to_tape (w₂ :: ws₂))) =
+        Part.some fun _ => list_to_tape (w₂ :: ws₂) := by
+      apply Routines.move_to_start_eval'
+      · intro i hi
+        by_contra h_exists_blank
+        let h_has_blank := List.mem_of_getElem h_exists_blank
+        let h_not_has_blank := blank_not_elem_list_to_string (ls := w₂ :: ws₂)
+        contradiction
+      · simp [list_to_string_cons]; omega
     intro i
     match i with
-    | 0 => simp [eq, h_part1, h_part2];  sorry
-    | 1 => simp [eq, h_part1, h_part2];  sorry
-    | 2 => simp [eq, h_part1, h_part2];  sorry
+    | 0 | 1 | 2 => simp [eq, h_part1, h_part2, h_move_w₁, h_move_w₂, h]
diff --git a/Complexity/Routines.lean b/Complexity/Routines.lean
index a98112c..cc9e749 100644
--- a/Complexity/Routines.lean
+++ b/Complexity/Routines.lean
@@ -105,6 +105,10 @@ lemma list_to_string_tail_nonempty
   (list_to_string ((c :: w) :: ws)).tail = (list_to_string (w :: ws)) := by
   simp [list_to_string, List.coe_schar]
 
+lemma blank_not_elem_list_to_string {ls : List (List Char)} :
+  SChar.blank ∉ list_to_string ls := by
+  simp [list_to_string, List.coe_schar]
+
 def list_to_tape (ls : List (List Char)) : Turing.Tape SChar :=
   Turing.Tape.mk₁ (list_to_string ls)