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..642bf7d
--- /dev/null
+++ b/Complexity/Eq.lean
@@ -0,0 +1,313 @@
+import Complexity.TuringMachine
+import Complexity.Dyadic
+import Complexity.TapeLemmas
+import Complexity.AbstractTape
+import Complexity.While
+import Complexity.Routines
+import Complexity.WithTapes
+import Complexity.TMComposition
+import Complexity.MoveUntil
+
+import Mathlib
+
+--- 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.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, Transition.step, Turing.Tape.mk₂, performTapeOps]
+  · dsimp
+    funext i
+    match i with
+    | 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
+    ⟨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₂, performTapeOps]
+  · dsimp
+    funext i
+    match i with
+    | 0 | 1 | 2 =>
+      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) :
+  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_all [eq_core, Transition.step, Turing.Tape.mk₂, performTapeOps]
+  · dsimp
+    funext i
+    match i with
+    | 0 | 1 | 2 =>
+      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) :
+  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
+
+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 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
+  (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 [
+      .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₁ (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 (w₁ w₂ : List Char) (h_neq : w₁ ≠ w₂) :
+  ∃ (common rest1 rest2 : List SChar), ∃ (a b : SChar),
+    (∀ c ∈ common, c ≠ .sep) ∧
+    (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
+  · -- 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
+    | 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 =>
+      -- contradiction with h_length: (c :: w₁).length ≤ [].length is false
+      simp at h_length
+    | cons d w₂' =>
+      by_cases h_char_eq : c = d
+      · -- 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₂) :
+  ∃ n ≤ min w₁.length w₂.length,
+  eq_core.eval [
+      list_to_tape (w₁ :: ws₁),
+      list_to_tape (w₂ :: ws₂),
+      .mk₂ [] (.blank :: list_to_string ([] :: ws₃))].get =
+    Part.some [
+      (.move .right)^[n] (list_to_tape (w₁ :: 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, 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
+  · 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
+      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
+      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₁ =
+                  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]
+  rw [Tape.move_right_append, Tape.move_right_append]
+  have h_common_no_sep' : .sep ∉ common := by
+    intro h_mem
+    exact h_common_no_sep .sep h_mem rfl
+  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
+
+
+--- 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.
+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 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
+    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₂]
+  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, 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_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 | 1 | 2 => simp [eq, h_part1, h_part2, h_move_w₁, h_move_w₂, h]
diff --git a/Complexity/MoveUntil.lean b/Complexity/MoveUntil.lean
index 8734800..b0a3b45 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,88 @@ 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)
+
+@[simp]
+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₁]
+
+@[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
diff --git a/Complexity/Routines.lean b/Complexity/Routines.lean
index ac40134..cc9e749 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]
@@ -101,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)
 
@@ -189,6 +197,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/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
diff --git a/Complexity/TuringMachine.lean b/Complexity/TuringMachine.lean
index 496ca31..e9e12ed 100644
--- a/Complexity/TuringMachine.lean
+++ b/Complexity/TuringMachine.lean
@@ -77,6 +77,19 @@ 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 := (Part.eq_some_iff.mp (h_eval 0)).1
+  rw [Part.eq_some_iff]
+  use h_dom
+  funext i
+  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.
 def TM.transforms_in_exact_time {k : ℕ} {Q Γ : Type*}
@@ -252,6 +265,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)
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)