diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
index 3985e270..334ba39e 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
@@ -16,6 +16,8 @@ public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
 public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
 public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
 
+import Mathlib.Tactic.FinCases
+
 namespace Turing
 
 variable {k : ℕ}
@@ -51,6 +53,80 @@ theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
   · simp [h]; grind
   · grind
 
+/-- The value of succ's eval_list at index j when applied via get. -/
+private lemma succ_eval_list_get_apply {k : ℕ} {i j : Fin k}
+    {tapes : Fin k → List (List OneTwo)}
+    (h : ((succ i).eval_list tapes).Dom) :
+    ((succ i).eval_list tapes).get h j =
+    (Function.update tapes i ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail)) j := by
+  sorry
+
+-- TODO we have to be much more radical.
+
+
+-- private lemma succ_space_at_iter {k : ℕ} (i : Fin k)
+--     (n : ℕ) (tapes : Fin k → List (List OneTwo)) :
+--   space_at_iter (tm := succ i) (by simp) n.succ tapes = Function.update (spaceUsed_init tapes)
+--       i
+--      -- TODO 1 + output size - some shortcut?
+--       i (1 + (spaceUsed_init ((succ i).eval_list_tot (by simp) tapes) i)) := by
+--   sorry
+
+
+-- theorem add₀_spaceUsed {tapes : Fin 6 → List (List OneTwo)} :
+--   add₀.spaceUsed_list tapes (h_halts := by sorry) = fun j : Fin 6 =>
+--     match j with
+--     | 0 => spaceUsed_init tapes 0
+--     | 1 => 1 + spaceUsed_init tapes 1
+--     | 2 => (dya (dya_inv ((tapes 0).headD []) +
+--              dya_inv ((tapes 1).headD [])) :: (tapes 2)).length + 1 + (spaceUsed_init tapes 2)
+--     | 3 => ((tapes 0).headD []).length + 1 + spaceUsed_init tapes 3
+--     | 4 => ((tapes 0).headD []).length + 1 + spaceUsed_init tapes 4
+--     | 5 => ((tapes 0).headD []).length + 1 + spaceUsed_init tapes 5 := by
+--   simp [add₀, spaceUsed_init_simp]
+--   funext j
+--   match j with
+--   | 0 => simp [spaceUsed_init_simp]
+--   | 1 => simp [spaceUsed_init_simp]
+--   | 2 => simp [spaceUsed_init_simp]
+--          sorry
+--   | 3 => sorry
+--   | 4 => sorry
+--   | 5 => sorry
+
+  -- -- Establish halting proofs for each component
+  -- have h_halts_copy : ∀ t : Fin 6 → BiTape (WithSep OneTwo),
+  --     (copy (k := 6) 1 2 (h_neq := by decide)).haltsOn t := by intro; sorry
+  -- have h_halts_loop : ∀ t : Fin 6 → BiTape (WithSep OneTwo),
+  --     (loop (h_i := by decide) (k := 3) 0 (succ (2 : Fin 3))).haltsOn t :=
+  --   loop_halts_of_halts succ_halts
+  -- -- Unfold add₀ = (copy 1 2) <;> loop 0 (succ 2), split space via seq
+  -- simp only [add₀, MultiTapeTM.seq_spaceUsed_list h_halts_copy h_halts_loop]
+  -- -- Compute the copy step's space usage and the intermediate tape state
+  -- simp only [copy_spaceUsed_list, copy_eval_list]
+  -- -- Expand the loop's space: aux tapes (≥3) get fixed formula, inner tapes (<3) use space_at_iter
+  -- simp only [loop_space_list (h_halts := succ_halts)]
+  -- -- Case analysis on tape index; apply succ_space_at_iter after j is concrete
+  -- funext ⟨j, hj⟩
+  -- match j, hj with
+  -- | 0, _ =>
+  --   simp only [succ_space_at_iter (2 : Fin 3) _ succ_halts]
+  --   simp [Function.update, Fin.ext_iff]
+  -- | 1, _ =>
+  --   simp only [succ_space_at_iter (2 : Fin 3) _ succ_halts]
+  --   simp [Function.update, Fin.ext_iff]
+  -- | 2, _ =>
+  --   simp only [succ_space_at_iter (2 : Fin 3) _ succ_halts]
+  --   simp only [succ_eval_list_get_apply, Part.get_some, Function.update,
+  --              Fin.ext_iff, listToString_length_cons]
+  --   simp (config := { decide := true }) only [if_true, dif_pos, List.headD_cons, List.tail_cons,
+  --              listToString_length_cons, spaceUsed_init_simp]
+  --   simp only [show (⟨1, (by omega : 1 < 6)⟩ : Fin 6) = 1 from rfl,
+  --              show (⟨2, (by omega : 2 < 6)⟩ : Fin 6) = 2 from rfl]
+  -- | 3, _ => simp [Function.update, Fin.ext_iff]
+  -- | 4, _ => simp [Function.update, Fin.ext_iff]
+  -- | 5, _ => simp [Function.update, Fin.ext_iff]
+
 /--
 A Turing machine that adds the heads of tapes i and j (in dyadic encoding) and pushes the result
 to tape l.
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
index 5a4345f5..45384244 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
@@ -373,6 +373,7 @@ public def eval_tot
   Fin k → BiTape Symbol :=
 (tm.eval tapes).get (h_alwaysHalts tapes)
 
+
 end MultiTapeTM
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean
index 566a3aef..81b7c49a 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean
@@ -28,6 +28,13 @@ lemma copy₁_eval_list {tapes : Fin 2 → List (List α)} :
     Part.some (Function.update tapes 1 (((tapes 0).headD []) :: tapes 1)) := by
   sorry
 
+@[simp]
+lemma copy₁_spaceUsed_list {tapes : Fin 2 → List (List α)} :
+  copy₁.spaceUsed_list (by simp) tapes = Function.update (Function.update (spaceUsed_init tapes)
+    0 (1 + (listToString (tapes 0)).length))
+    1 (listToString (((tapes 0).headD []) :: tapes 1)).length := by
+  sorry
+
 /--
 A Turing machine that copies the first word on tape `i` to tape `j`.
 If Tape `i` is empty, pushes the empty word to tape `j`.
@@ -48,6 +55,16 @@ public lemma copy_eval_list
   simp_all [copy]
   grind
 
+@[simp]
+public lemma copy_spaceUsed_list {k : ℕ} (i j : Fin k)
+  (h_inj : [i, j].get.Injective := by intro x y; grind)
+  {tapes : Fin k → List (List α)} :
+  (copy i j h_inj).spaceUsed_list (by simp) tapes =
+    Function.update (Function.update (spaceUsed_init tapes)
+    i (1 + (listToString (tapes i)).length))
+    j (listToString (((tapes i).headD []) :: tapes j)).length := by
+  sorry
+
 end Routines
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean b/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean
index 3dbba8fb..25435293 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean
@@ -35,7 +35,7 @@ public def HeadStats.space (hs : HeadStats) : ℕ :=
 
 
 /-- Compute the head statistics for a turing machine starting with a certain tape configuration. -/
-public def headStats (tm : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) :
+public def MultiTapeTM.headStats (tm : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) :
   Part (Fin k → HeadStats) := sorry
 
 /-- Execute a Turing machine and also compute head statistics. -/
@@ -53,7 +53,16 @@ def seq_combine_stats (stats₁ stats₂ : Fin k → HeadStats) : Fin k → Head
     final₁ + final₂,
     by omega⟩
 
-lemma seq_evalWithStats (tm₁ tm₂ : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) (i : Fin k) :
+lemma seq_stats (tm₁ tm₂ : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) (i : Fin k) :
+  (seq tm₁ tm₂).headStats tapes = do
+      let stats₁ ← tm₁.headStats tapes
+      let stats₂ ← tm₂.headStats tapes'
+      return seq_combine_stats stats₁ stats₂ := by sorry
+
+lemma seq_evalWithStats
+    (tm₁ tm₂ : MultiTapeTM k Symbol)
+    (tapes : Fin k → BiTape Symbol)
+    (i : Fin k) :
   (seq tm₁ tm₂).evalWithStats tapes = do
       let (tapes', stats₁) ← tm₁.evalWithStats tapes
       let (tapes'', stats₂) ← tm₂.evalWithStats tapes'
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean
index 265f9e42..b091813b 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean
@@ -31,5 +31,16 @@ public theorem isZero_eval_list {i : Fin k} {tapes : Fin k → List (List OneTwo
   simp [isZero]
   grind
 
+@[simp]
+public theorem isZero_spaceUsed_list {i j : Fin k} {tapes : Fin k → List (List OneTwo)} :
+  (isZero i).spaceUsed_list (by simp [isZero]) tapes = Function.update (spaceUsed_init tapes) i
+    (if (tapes i).headD [] = [] then
+      (listToString ([OneTwo.one] :: (tapes i).tail)).length
+    else
+      (listToString (tapes i)).length) := by
+  simp [isZero, spaceUsed_init_simp]
+  sorry
+
+
 end Routines
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean
index 9d9d41b9..0f6f2ca1 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean
@@ -26,6 +26,15 @@ public def ite (i : Fin k) (tm₁ tm₂ : MultiTapeTM k (WithSep α)) :
   q₀ := PUnit.unit
   tr _ syms := sorry
 
+@[simp]
+public theorem ite_halts
+  {i : Fin k}
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  (h_tm₁_halts : ∀ tapes, tm₁.HaltsOnLists tapes)
+  (h_tm₂_halts : ∀ tapes, tm₂.HaltsOnLists tapes) :
+  ∀ tapes, (ite i tm₁ tm₂).HaltsOnLists tapes := by
+  sorry
+
 @[simp, grind =]
 public theorem ite_eval_list
   {i : Fin k}
@@ -35,6 +44,20 @@ public theorem ite_eval_list
     if (tapes i).headD [] = [] then tm₂.eval_list tapes else tm₁.eval_list tapes := by
   sorry
 
+@[simp]
+public theorem ite_spaceUsed_list
+  {i : Fin k}
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  (h_tm₁_halts : ∀ tapes, tm₁.HaltsOnLists tapes)
+  (h_tm₂_halts : ∀ tapes, tm₂.HaltsOnLists tapes)
+  {tapes : Fin k → List (List α)} :
+  (ite i tm₁ tm₂).spaceUsed_list (by simp [h_tm₁_halts, h_tm₂_halts]) tapes =
+    if (tapes i).headD [] = [] then
+      tm₂.spaceUsed_list h_tm₂_halts tapes
+    else
+      tm₁.spaceUsed_list h_tm₁_halts tapes := by
+  sorry
+
 end Routines
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
index bcca09ed..0fb1ca54 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
@@ -56,6 +56,18 @@ public def stringToList (s : List (Option (WithSep Symbol))) : Option (List (Lis
         | w :: rest => some ((c :: w) :: rest)))
   (some [])
 
+@[simp, grind =]
+public theorem listToString_length_nil :
+    (listToString ([] : List (List Symbol))).length = 0 := by
+  simp [listToString]
+
+@[simp, grind =]
+public theorem listToString_length_cons
+    (w : List Symbol) (ls : List (List Symbol)) :
+    (listToString (w :: ls)).length = w.length + 1 + (listToString ls).length := by
+  simp [listToString]
+  grind
+
 /-- Encodes a list of words into a tape. -/
 public def listToTape (ls : List (List Symbol)) : BiTape (WithSep Symbol) :=
   BiTape.mk₁ (listToString ls)
@@ -95,6 +107,14 @@ public def MultiTapeTM.eval_list
     Part (Fin k → List (List Symbol)) :=
   (tm.eval (listToTape ∘ tapes)).bind fun tapes => tapesToLists tapes
 
+@[simp]
+public def MultiTapeTM.HaltsOnLists_of_evalList_eq_some
+    (tm : MultiTapeTM k (WithSep Symbol))
+    (tapes : Fin k → List (List Symbol))
+    (h_eval : (tm.eval_list tapes).Dom) :
+  tm.HaltsOnLists tapes := by
+  sorry
+
 @[simp]
 public theorem MultiTapeTM.HaltsOnLists_of_eval_list
     {tm : MultiTapeTM k (WithSep Symbol)}
@@ -121,6 +141,15 @@ public def MultiTapeTM.eval_list_tot
   Fin k → List (List Symbol) :=
     (tm.eval_list tapes).get (tm.eval_list_dom_of_halts_on_lists (h_alwaysHalts tapes))
 
+@[simp]
+public lemma MultiTapeTM.eval_list_tot_eq
+    (tm : MultiTapeTM k (WithSep Symbol))
+    (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes)
+    (tapes : Fin k → List (List Symbol)) :
+  (tm.eval_list_tot) h_alwaysHalts tapes =
+    (tm.eval_list tapes).get (tm.eval_list_dom_of_halts_on_lists (h_alwaysHalts tapes)) := by
+  simp
+
 @[simp, grind =]
 public theorem MultiTapeTM.extend_eval_list
     {k₁ k₂ : ℕ} {h_le : k₁ ≤ k₂}
@@ -155,6 +184,20 @@ public theorem MultiTapeTM.with_tapes_eval_list
 --     (ts : (Fin k → List (List Symbol)) × (Fin k → HeadStats)) : Prop :=
 --     tm.evalWithStats (listToTape ∘ tapes) = .some (listToTape ∘ ts.1, ts.2)
 
+/-- Head statistics for list computations.
+The assumption is that the head starts on the leftmost symbol of the initial tape and ends on the
+leftmost symbol of the final tape. The zero-point is the right-most non-blank symbol of the initial
+tape which is the same point as the right-most non-blank symbol of the final tape.
+The head never moves right of the zero point and it moves at most `leftmost` points left of the
+zero point. -/
+public structure HeadStatsList where
+  /-- The number of symbols on the initial tape. TODO isn't this redundant? -/
+  initialLength : ℕ
+  /-- The number of symbols on the tape after termination. TODO isn't this redundant? -/
+  finalLength : ℕ
+  /-- The left-most position of the head in number of symbols left of the zero point. -/
+  leftmost : ℕ
+
 -- /--
 -- Evaluate the Turing machine `tm` on the list-encoded tapes `tapes` and also return the head
 -- statistics of the computation.
@@ -165,6 +208,35 @@ public theorem MultiTapeTM.with_tapes_eval_list
 --     Part ((Fin k → List (List Symbol)) × (Fin k → HeadStats)) :=
 --   ⟨∃ ts, tm.TransformsListsWithStats tapes ts, fun h => h.choose⟩
 
+-- TODO we could also use "tape cells moved over" or "added".
+-- the benefit is that we could say `0` if the head did not move at all or only deleted symbols.
+-- the problem is that the situation of adding symbols is more complicated.
+
+/-- The max number of tape cells the head traversed over or that contain non-blank symbols.
+Note that the head will always be left of or on the "zero" point which is the initial position
+for an empty initial tape or the rightmost non-blank cell. -/
+-- TODO we could even make this Part now.
+public def MultiTapeTM.spaceUsed_list
+    (tm : MultiTapeTM k (WithSep Symbol))
+    (h_halts : ∀ tapes, tm.HaltsOnLists tapes := by simp)
+    (tapes : Fin k → List (List Symbol)) : Fin k → ℕ := sorry
+
+/-- The space initially used by a Turing machine that has the given tape configuration. -/
+public def spaceUsed_init (tapes : Fin k → List (List Symbol)) : Fin k → ℕ := fun i =>
+  (listToString (tapes i)).length
+
+public def spaceUsed_init_simp (tapes : Fin k → List (List Symbol)) (i : Fin k) :
+  spaceUsed_init tapes i = (listToString (tapes i)).length := by simp [spaceUsed_init]
+
+@[simp]
+public lemma spaceUsed_init_le_spaceUsed
+  {tm : MultiTapeTM k (WithSep Symbol)}
+  (h_halts : ∀ tapes, tm.HaltsOnLists tapes := by simp)
+  (tapes : Fin k → List (List Symbol))
+  (i : Fin k) :
+  spaceUsed_init tapes i ≤ MultiTapeTM.spaceUsed_list tm h_halts tapes i := by
+  sorry
+
 -- TODO for machines running on lists, we can actually have more precise head stats:
 -- we know (and should enforce) that the head never moves to the right of the rightmost symbol
 -- and always starts and ends on the leftmost symbol (and if the tape is empty, it never moves
@@ -215,4 +287,13 @@ public lemma dya_inv_dya (n : ℕ) : dya_inv (dya n) = n := by sorry
 @[simp, grind =]
 public lemma dya_dya_inv (w : List OneTwo) : dya (dya_inv w) = w := by sorry
 
+@[simp, grind =]
+public theorem MultiTapeTM.with_tapes_spaceUsed
+  {Symbol : Type} [Fintype Symbol] [Inhabited Symbol]
+  {k₁ k₂ : ℕ}
+  {tm : MultiTapeTM k₁ (WithSep Symbol)} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective}
+  {tapes : Fin k₂ → List (List Symbol)} :
+  (tm.with_tapes f h_inj).spaceUsed_list tapes (h_halts := sorry) =
+    apply_updates (spaceUsed_init tapes) (tm.spaceUsed_list (tapes ∘ f) (h_halts := sorry)) f := by
+  sorry
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
index 217f62a3..31cbcad2 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
@@ -9,6 +9,8 @@ module
 public import Cslib.Computability.Machines.MultiTapeTuring.Basic
 public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
 
+public import Mathlib.Order.Monotone.Defs
+
 namespace Turing
 
 namespace Routines
@@ -55,5 +57,67 @@ public theorem loop_halts_of_halts {i : Fin k}
   ∀ tapes, (loop i tm).HaltsOnLists tapes := by
   sorry
 
+public def space_at_iter {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (h_halts : ∀ tapes, tm.HaltsOnLists tapes)
+  (iteration : ℕ)
+  (tapes : Fin k → List (List OneTwo)) : Fin k → ℕ :=
+  match iteration with
+  | 0 => spaceUsed_init tapes
+  | Nat.succ iter => fun i => max
+      (space_at_iter h_halts iter tapes i)
+      (tm.spaceUsed_list h_halts ((tm.eval_list_tot h_halts)^[iter] tapes) i)
+
+@[simp]
+public theorem space_at_iter_of_mono {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (h_halts : ∀ tapes, tm.HaltsOnLists tapes)
+  (i : Fin k)
+  (h_mono_step : ∀ tapes, tm.spaceUsed_list h_halts tapes i ≤
+     tm.spaceUsed_list h_halts (tm.eval_list_tot h_halts tapes) i)
+  (iteration : ℕ)
+  (tapes : Fin k → List (List OneTwo)) :
+  space_at_iter h_halts iteration.succ tapes i = tm.spaceUsed_list h_halts
+      ((tm.eval_list_tot h_halts)^[iteration] tapes) i := by
+  induction iteration generalizing tapes with
+  | zero => simp [space_at_iter]
+  | succ iter ih =>
+    sorry
+    -- unfold space_at_iter
+    -- rw [ih]
+    -- simp only [Function.iterate_succ', Function.comp_apply, sup_eq_right, h_mono_step]
+
+@[simp]
+public theorem space_at_iter_of_constant {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  {h_halts : ∀ tapes, tm.HaltsOnLists tapes}
+  {i : Fin k}
+  (h_constant_space : ∀ tapes, tm.spaceUsed_list h_halts tapes i = spaceUsed_init tapes i)
+  (h_constant_semantics : ∀ tapes, ((tm.eval_list tapes).map fun t => t i) = .some (tapes i))
+  {iteration : ℕ}
+  {tapes : Fin k → List (List OneTwo)} :
+  space_at_iter h_halts iteration tapes i = spaceUsed_init tapes i := by
+  induction iteration generalizing tapes with
+  | zero => simp [space_at_iter]
+  | succ iter ih =>
+    unfold space_at_iter
+    have h_id : (fun tapes : Fin k → List (List OneTwo) => tapes) = id := rfl
+    rw [ih]
+    simp [h_constant_space, h_constant_semantics, h_id, Function.iterate_id]
+    sorry
+
+@[simp]
+public theorem loop_space_list {i : Fin k}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  {h_halts : ∀ tapes, tm.HaltsOnLists tapes}
+  {tapes : Fin (k + 3) → List (List OneTwo)} :
+  (loop i tm).spaceUsed_list (by simp [h_halts]) tapes = (fun j : Fin (k + 3) =>
+      (if h : j < k then
+        space_at_iter h_halts
+          (dya_inv ((tapes ⟨i, by omega⟩).headD [])) (fun i => tapes ⟨i, by omega⟩) ⟨j, h⟩
+      else
+        ((tapes ⟨i, by omega⟩).headD []).length + 1 + (spaceUsed_init tapes j))) := by
+  sorry
+
 end Routines
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean
index a18b72b9..262e262b 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean
@@ -27,6 +27,11 @@ lemma pop₁_eval_list {tapes : Fin 1 → List (List α)} :
   pop₁.eval_list tapes = .some (Function.update tapes 0 (tapes 0).tail) := by
   sorry
 
+@[simp]
+lemma pop₁_spaceUsed_list {tapes : Fin 1 → List (List α)} :
+    (pop₁ (α := α)).spaceUsed_list (by simp) tapes = spaceUsed_init tapes := by
+  sorry
+
 /--
 A Turing machine that removes the first word on tape `i`. If the tape is empty, does nothing.
 -/
@@ -40,6 +45,13 @@ public theorem pop_eval_list {k : ℕ} {i : Fin k}
   have h_inj : [i].get.Injective := by intro x y; grind
   simp_all [pop]
 
+@[simp]
+public theorem pop_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List α)} :
+  (pop i).spaceUsed_list (by simp) tapes = spaceUsed_init tapes := by
+  have h_inj : [i].get.Injective := by intro x y; grind
+  sorry
+
+
 end Routines
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean
index d6c0bac7..85b63af1 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean
@@ -27,6 +27,11 @@ lemma push₁_eval_list {w : List α} {tapes : Fin 1 → List (List α)} :
   (push₁ w).eval_list tapes = .some (Function.update tapes 0 (w :: (tapes 0))) := by
   sorry
 
+@[simp]
+lemma push₁_spaceUsed_list {w : List α} {tapes : Fin 1 → List (List α)} {i : Fin 1} :
+    (push₁ w).spaceUsed_list (by simp) tapes i = (listToString (w :: (tapes 0))).length := by
+  sorry
+
 /--
 A Turing machine that pushes the word `w` to tape `i`.
 -/
@@ -41,6 +46,15 @@ public theorem push_eval_list {k : ℕ}
   have h_inj : [i].get.Injective := by intro x y; grind
   simp_all [push]
 
+@[simp]
+public theorem push_spaceUsed_list {k : ℕ} {i : Fin k} {w : List α}
+  {tapes : Fin k → List (List α)} :
+    (push i w).spaceUsed_list (by simp) tapes = Function.update (spaceUsed_init tapes)
+      i (listToString (w :: (tapes i))).length := by
+  simp [push]
+  sorry
+
+
 end Routines
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean
index e39726df..6a687e59 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean
@@ -46,6 +46,25 @@ public theorem seq_associative
   (seq (seq tm₁ tm₂) tm₃).eval = (seq tm₁ (seq tm₂ tm₃)).eval := by
   sorry
 
+@[simp]
+public theorem seq_halts_of_halts
+  {tm₁ tm₂ : MultiTapeTM k (WithSep Symbol)}
+  (h_halts₁ : ∀ tapes, tm₁.HaltsOnLists tapes)
+  (h_halts₂ : ∀ tapes, tm₂.HaltsOnLists tapes) :
+  ∀ tapes, (seq tm₁ tm₂).HaltsOnLists tapes := by
+  sorry
+
+@[simp]
+public theorem seq_spaceUsed_list
+  {tm₁ tm₂ : MultiTapeTM k (WithSep Symbol)}
+  (h_halts₁ : ∀ tapes, tm₁.HaltsOnLists tapes)
+  (h_halts₂ : ∀ tapes, tm₂.HaltsOnLists tapes)
+  {tapes₀ : Fin k → List (List Symbol)} :
+  (seq tm₁ tm₂).spaceUsed_list (by simp [h_halts₁, h_halts₂]) tapes₀ = fun i =>
+    let tapes₁ := tm₁.eval_list_tot h_halts₁ tapes₀
+    max (tm₁.spaceUsed_list h_halts₁ tapes₀ i) (tm₂.spaceUsed_list h_halts₂ tapes₁ i)
+  := by sorry
+
 /--
 Sequential combination of Turing machines.
 -/
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
index 0ed3fc41..8c0bfb3d 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
@@ -12,6 +12,7 @@ import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Computability.Machines.MultiTapeTuring.Basic
 public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
 public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
+public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
 
 import Mathlib.Data.Nat.Bits
 
@@ -54,6 +55,23 @@ public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (Lis
 --         [⟨-1, (dya n).length, -1, by omega⟩].get) := by
 --   sorry
 
+@[simp, grind =]
+public lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
+  (succ i).spaceUsed_list (by simp) tapes = Function.update (spaceUsed_init tapes) i
+    (1 + ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail).length) := by
+  sorry
+  --   (if (dya (dya_inv ((tapes i).headD [])).succ).length = ((tapes i).headD []).length then
+  --     1 + (listToString (tapes i)).length -- We need to move at least one char to the left.
+  --   else
+  --     2 + (listToString (tapes i)).length) -- We need to move at least one char to the left
+  -- := by sorry
+
+@[simp]
+public lemma succ_spaceUsed_mono_iter {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
+  (succ i).spaceUsed_list (by simp) tapes i ≤
+    (succ i).spaceUsed_list (by simp) ((succ i).eval_list_tot (by simp) tapes) i := by
+  simp
+
 
 end Routines
 
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean b/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean
index 209179db..e6d443e9 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean
@@ -9,12 +9,13 @@ module
 public import Cslib.Computability.Machines.MultiTapeTuring.Basic
 public import Cslib.Computability.Machines.MultiTapeTuring.TapeExtension
 
+
 public import Mathlib.Logic.Equiv.Fintype
 public import Mathlib.Data.Finset.Sort
 
 namespace Turing
 
-variable [Inhabited α] [Fintype α]
+variable [Inhabited Symbol] [Fintype Symbol]
 
 variable {k : ℕ}
 
@@ -22,7 +23,7 @@ variable {k : ℕ}
 Permute tapes according to a bijection.
 -/
 public def MultiTapeTM.permute_tapes
-  (tm : MultiTapeTM k α) (σ : Equiv.Perm (Fin k)) : MultiTapeTM k α where
+  (tm : MultiTapeTM k Symbol) (σ : Equiv.Perm (Fin k)) : MultiTapeTM k Symbol where
   State := tm.State
   stateFintype := tm.stateFintype
   q₀ := tm.q₀
@@ -32,7 +33,7 @@ public def MultiTapeTM.permute_tapes
 --- General theorem: permuting tapes commutes with evaluation
 @[simp, grind =]
 public theorem MultiTapeTM.permute_tapes_eval
-  (tm : MultiTapeTM k α) (σ : Equiv.Perm (Fin k)) (tapes : Fin k → BiTape α) :
+  (tm : MultiTapeTM k Symbol) (σ : Equiv.Perm (Fin k)) (tapes : Fin k → BiTape Symbol) :
   (tm.permute_tapes σ).eval tapes =
     (tm.eval (tapes ∘ σ)).map (fun tapes' => tapes' ∘ σ.symm) := by
   sorry
@@ -66,10 +67,19 @@ has the right amount of tapes.
 -/
 public def MultiTapeTM.with_tapes {k₁ k₂ : ℕ}
 -- TODO use embedding instead?
-  (tm : MultiTapeTM k₁ α) (f : Fin k₁ → Fin k₂) (h_inj : f.Injective) : MultiTapeTM k₂ α :=
+  (tm : MultiTapeTM k₁ Symbol)
+  (f : Fin k₁ → Fin k₂)
+  (h_inj : f.Injective) : MultiTapeTM k₂ Symbol :=
   (tm.extend
     (by simpa using Fintype.card_le_of_injective f h_inj)).permute_tapes (inj_to_perm f h_inj)
 
+@[simp]
+public theorem MultiTapeTM.with_tapes_halts_of_halts {k₁ k₂ : ℕ}
+  (tm : MultiTapeTM k₁ Symbol) (f : Fin k₁ → Fin k₂) (h_inj : f.Injective)
+  (h_halts : ∀ tapes, tm.HaltsOn tapes) :
+  ∀ tapes, (tm.with_tapes f h_inj).HaltsOn tapes := by
+  sorry
+
 -- TODO do not use `h.choose` here but rather assume that `f` is injective.
 
 /--
@@ -112,11 +122,26 @@ public lemma apply_updates_function_update
   funext i
   apply apply_updates_function_update_apply h_inj
 
+-- TODO tagging this @simp will use this instead of the two above,
+-- which can lead to a dead-end.
+public lemma apply_updates_function
+  {γ : Type}
+  {k₁ k₂ : ℕ}
+  {tapes : Fin k₂ → γ}
+  {tapes' : Fin k₁ → γ}
+  {f : Fin k₁ → Fin k₂}
+  (h_inj : f.Injective) :
+  apply_updates tapes tapes' f = fun i =>
+    if h : ∃ j, f j = i then tapes' h.choose else tapes i := by
+  unfold apply_updates
+  simp
+
+
 @[simp, grind =]
 public theorem MultiTapeTM.with_tapes_eval
   {k₁ k₂ : ℕ}
-  {tm : MultiTapeTM k₁ α} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective}
-  {tapes : Fin k₂ → BiTape α} :
+  {tm : MultiTapeTM k₁ Symbol} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective}
+  {tapes : Fin k₂ → BiTape Symbol} :
   (tm.with_tapes f h_inj).eval tapes =
     (tm.eval (tapes ∘ f)).map
       (fun tapes' => fun t => apply_updates tapes tapes' f t) := by
@@ -124,4 +149,5 @@ public theorem MultiTapeTM.with_tapes_eval
   sorry
 
 
+
 end Turing