From 84c0bdcdfccdc963aaa46cbe16ec22197c88aad0 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 3 Mar 2026 16:25:13 +0100
Subject: [PATCH 1/4] Space requirements.

---
 .../Machines/MultiTapeTuring/AddRoutine.lean  | 11 ++++
 .../Machines/MultiTapeTuring/Basic.lean       |  5 ++
 .../Machines/MultiTapeTuring/CopyRoutine.lean | 31 +++++++++++
 .../Machines/MultiTapeTuring/HeadStats.lean   |  8 ++-
 .../MultiTapeTuring/IsZeroRoutine.lean        | 22 ++++++++
 .../MultiTapeTuring/IteCombinator.lean        | 21 ++++++++
 .../MultiTapeTuring/ListEncoding.lean         | 53 +++++++++++++++++++
 .../MultiTapeTuring/LoopCombinator.lean       | 51 ++++++++++++++++++
 .../Machines/MultiTapeTuring/PopRoutine.lean  | 19 +++++++
 .../Machines/MultiTapeTuring/PushRoutine.lean | 20 +++++++
 .../MultiTapeTuring/SequentialCombinator.lean | 19 +++++++
 .../Machines/MultiTapeTuring/SuccRoutine.lean | 10 ++++
 .../Machines/MultiTapeTuring/WithTapes.lean   | 24 +++++++++
 13 files changed, 293 insertions(+), 1 deletion(-)

diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
index 3cc0737f..0afa4143 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
@@ -51,6 +51,17 @@ theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
   · simp [h]; grind
   · grind
 
+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 => 1 + spaceUsed_init tapes 0
+    | 1 => 1 + spaceUsed_init tapes 1
+    | 2 => 1 + ((dya (dya_inv ((tapes 2).headD [])).succ) :: (tapes 2).tail).length
+    | 3 => 1 + ((tapes 3).headD []).length + spaceUsed_init tapes 3
+    | 4 => 1 + ((tapes 4).headD []).length + spaceUsed_init tapes 4
+    | 5 => 1 + ((tapes 5).headD []).length + spaceUsed_init tapes 5 := by
+  sorry
+
 /--
 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 5d1f0464..9fac06d3 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
@@ -371,6 +371,11 @@ def OutputsWithinTime (tm : MultiTapeTM k α) (l l' : List α) (m : ℕ) :=
 --   grind [hevals.apply_le_apply_add (Cfg.space_used tm)
 --       fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)]
 
+structure MultiTapeTotalTM k α extends MultiTapeTM k α where
+  /-- The Turing machine halts on all inputs. -/
+  haltsOn : ∀ tapes, toMultiTapeTM.haltsOn tapes
+
+
 end MultiTapeTM
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean
index 96a71504..2c30e666 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean
@@ -27,6 +27,19 @@ 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₁_halts {tapes : Fin 2 → BiTape (WithSep α)} :
+  copy₁.haltsOn tapes := by
+  sorry
+
+@[simp]
+lemma copy₁_spaceUsed_list {tapes : Fin 2 → List (List α)} :
+  copy₁.spaceUsed_list 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`.
@@ -38,6 +51,12 @@ public def copy {k : ℕ} (i j : ℕ)
   MultiTapeTM k (WithSep α) :=
   copy₁.with_tapes [⟨i, h_i_lt⟩, ⟨j, h_j_lt⟩].get (by intro x y; grind)
 
+@[simp]
+public lemma copy_halts {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
+  {tapes : Fin k → BiTape (WithSep α)} :
+  (copy i j (h_neq := h_neq) (h_i_lt) (h_j_lt)).haltsOn tapes = true := by
+  simp [copy]
+
 @[simp, grind =]
 public lemma copy_eval_list
   {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
@@ -48,6 +67,18 @@ public lemma copy_eval_list
   have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind
   simp_all [copy]
 
+@[simp]
+public lemma copy_spaceUsed_list
+  {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
+  {tapes : Fin k → List (List α)} :
+  (copy i j h_neq h_i_lt h_j_lt).spaceUsed_list tapes (by simp [copy]) =
+    Function.update (Function.update (spaceUsed_init tapes)
+    ⟨i, h_i_lt⟩ (1 + (listToString (tapes ⟨i, h_i_lt⟩)).length))
+    ⟨j, h_j_lt⟩ (listToString (((tapes ⟨i, h_i_lt⟩).headD []) :: tapes ⟨j, h_j_lt⟩)).length := by
+  have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind
+  simp_all [copy, apply_updates_function]
+  grind
+
 end Routines
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean b/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean
index d0ea26b2..882d8226 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean
@@ -37,7 +37,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 α) (tapes : Fin k → BiTape α) :
+public def MultiTapeTM.headStats (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) :
   Part (Fin k → HeadStats) := sorry
 
 /-- Execute a Turing machine and also compute head statistics. -/
@@ -55,6 +55,12 @@ def seq_combine_stats (stats₁ stats₂ : Fin k → HeadStats) : Fin k → Head
     final₁ + final₂,
     by omega⟩
 
+lemma seq_stats (tm₁ tm₂ : MultiTapeTM k α) (tapes : Fin k → BiTape α) (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 α) (tapes : Fin k → BiTape α) (i : Fin k) :
   (seq tm₁ tm₂).evalWithStats tapes = do
       let (tapes', stats₁) ← tm₁.evalWithStats tapes
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean
index fcd35f7b..d11ad726 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean
@@ -31,5 +31,27 @@ 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 tapes (by simp [isZero]) = 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 only [isZero, ite_spaceUsed_list]
+  by_cases h : j = i
+  · simp only [List.headD_eq_head?_getD, pop_halts, implies_true, push_halts_on,
+    MultiTapeTM.seq_spaceUsed_list, pop_spaceUsed, pop_eval_list, Part.get_some,
+    push_spaceUsed_list, Function.update_self, listToString_length_cons, List.length_cons,
+    List.length_nil, zero_add, Nat.reduceAdd]
+    sorry
+    -- cases (tapes i) with
+    -- | nil =>  grind
+    -- | cons hd tl => grind
+  · simp [h]
+    -- grind
+    sorry
+
+
 end Routines
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean
index e0bf71b8..280fec62 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₀ := 0
   M _ syms := sorry
 
+@[simp]
+public theorem ite_halts
+  {i : Fin k}
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  (h_tm₁_halts : ∀ tapes, tm₁.haltsOn tapes)
+  (h_tm₂_halts : ∀ tapes, tm₂.haltsOn tapes) :
+  ∀ tapes, (ite i tm₁ tm₂).haltsOn tapes := by
+  sorry
+
 @[simp, grind =]
 public theorem ite_eval_list
   {i : Fin k}
@@ -35,6 +44,18 @@ 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 α)}
+  {tapes : Fin k → List (List α)} :
+  (ite i tm₁ tm₂).spaceUsed_list tapes sorry =
+    if (tapes i).headD [] = [] then
+      tm₂.spaceUsed_list tapes sorry
+    else
+      tm₁.spaceUsed_list tapes sorry := by
+  sorry
+
 end Routines
 
 end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
index 7e44e4d3..16f3a951 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
@@ -42,6 +42,18 @@ of the resulting string (if the list is non-empty). -/
 public def listToString (ls : List (List α)) : List (WithSep α) :=
   (ls.map (fun w : List α => (w.map .ofChar) ++ [.comma])).flatten
 
+@[simp, grind =]
+public theorem listToString_length_nil :
+    (listToString ([] : List (List α))).length = 0 := by
+  simp [listToString]
+
+@[simp, grind =]
+public theorem listToString_length_cons
+    (w : List α) (ls : List (List α)) :
+    (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 α)) : BiTape (WithSep α) :=
   BiTape.mk₁ (listToString ls)
@@ -118,6 +130,20 @@ def MultiTapeTM.TransformsListsWithStats
     (ts : (Fin k → List (List α)) × (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.
@@ -128,6 +154,24 @@ public noncomputable def MultiTapeTM.evalWithStats_list
     Part ((Fin k → List (List α)) × (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 noncomputable def MultiTapeTM.spaceUsed_list
+    (tm : MultiTapeTM k (WithSep α))
+    (tapes : Fin k → List (List α))
+    (h_halts : ∀ tapes, tm.haltsOn tapes := by simp) : Fin k → ℕ := sorry
+
+/-- The space initially used by a Turing machine that has the given tape configuration. -/
+@[simp] -- TODO do we need simp here?
+public def spaceUsed_init (tapes : Fin k → List (List α)) : Fin k → ℕ := fun i =>
+  (listToString (tapes i)).length
+
 -- 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
@@ -176,4 +220,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
+  {α : Type} [Fintype α] [Inhabited α]
+  {k₁ k₂ : ℕ}
+  {tm : MultiTapeTM k₁ (WithSep α)} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective}
+  {tapes : Fin k₂ → List (List α)} :
+  (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 c4cf18f0..1d30d192 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
@@ -48,5 +50,54 @@ public theorem loop_eval_list {i : ℕ} {h_i : i < k}
           fun tapes' => tapes_extend_by tapes' tapes := by
   sorry
 
+public theorem loop_halts_of_halts
+  {i : ℕ} {h_i : i < k}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (h_halts : ∀ tapes, tm.haltsOn tapes) :
+  ∀ tapes, (loop i tm (h_i := h_i)).haltsOn tapes := by
+  sorry
+
+public noncomputable def space_at_iter {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (h_halts : ∀ tapes, tm.haltsOn 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
+        ((fun tapes => (tm.eval_list tapes).get (by sorry))^[iter] tapes) h_halts i)
+
+-- TODO the following is probably not true for aux tapes. There we might need a bound.
+
+@[simp]
+public lemma space_at_iter_of_mono {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (h_halts : ∀ tapes, tm.haltsOn tapes)
+  (i : Fin k)
+  -- The machine does not delete anything on the tape.
+  (h_mono_output : ∀ tapes, (tapes i).length ≤ ((tm.eval_list tapes).get (by sorry) i).length)
+  -- The machine does not have any exess space usage
+  (h_mono_space : ∀ tapes, (spaceUsed_init tapes i) =
+      ((tm.eval_list tapes).get (by sorry) i).length)
+  (iteration : ℕ)
+  (tapes : Fin k → List (List OneTwo)) :
+  space_at_iter h_halts iteration tapes i = ((tm.eval_list tapes).get (by sorry) i).length := by
+  sorry
+
+@[simp]
+public theorem loop_space_list {i : ℕ} {h_i : i < k}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  {h_halts : ∀ tapes, tm.haltsOn tapes}
+  {tapes : Fin (k + 3) → List (List OneTwo)} :
+  (loop i tm (h_i := h_i)).spaceUsed_list tapes sorry = (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, sorry⟩) ⟨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 7b615a0d..fa3b38c4 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean
@@ -26,6 +26,14 @@ 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₁_halts_on : ∀ tapes, (pop₁ (α := α)).haltsOn tapes := by sorry
+
+@[simp]
+lemma pop₁_spaceUsed_list {tapes : Fin 1 → List (List α)} :
+    (pop₁ (α := α)).spaceUsed_list tapes = spaceUsed_init tapes := by
+  sorry
+
 /--
 A Turing machine that removes the first word on tape `i`. If the tape is empty, does nothing.
 -/
@@ -39,6 +47,17 @@ 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_halts {k : ℕ} {i : Fin k} : ∀ tapes, (pop i (α := α)).haltsOn tapes := by
+  simp [pop]
+
+@[simp]
+public theorem pop_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List α)} :
+  (pop i).spaceUsed_list tapes (h_halts := pop_halts) = 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 c703a1e4..42fe0796 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean
@@ -26,6 +26,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 tapes sorry i = (listToString (w :: (tapes 0))).length := by
+  sorry
+
 /--
 A Turing machine that pushes the word `w` to tape `i`.
 -/
@@ -40,6 +45,21 @@ public theorem push_eval_list {k : ℕ}
   have h_inj : [i].get.Injective := by intro x y; grind
   simp_all [push]
 
+@[simp]
+public theorem push_halts_on {k : ℕ} {i : Fin k} {w : List α} :
+  ∀ tapes, (push i w).haltsOn tapes := by
+  sorry
+
+
+@[simp]
+public theorem push_spaceUsed_list {k : ℕ} {i : Fin k} {w : List α}
+  {tapes : Fin k → List (List α)} :
+    (push i w).spaceUsed_list 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 dba01653..149d1b4d 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 α}
+  (h_halts₁ : ∀ tapes, tm₁.haltsOn tapes)
+  (h_halts₂ : ∀ tapes, tm₂.haltsOn tapes) :
+  ∀ tapes, (seq tm₁ tm₂).haltsOn tapes := by
+  sorry
+
+@[simp]
+public theorem seq_spaceUsed_list
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  (h_halts₁ : ∀ tapes, tm₁.haltsOn tapes)
+  (h_halts₂ : ∀ tapes, tm₂.haltsOn tapes)
+  {tapes₀ : Fin k → List (List α)} :
+  (seq tm₁ tm₂).spaceUsed_list tapes₀ sorry = fun i =>
+    let tapes₁ := (tm₁.eval_list tapes₀).get sorry
+    max (tm₁.spaceUsed_list tapes₀ h_halts₁ i) (tm₂.spaceUsed_list tapes₁ h_halts₂ 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 8c4f6bb9..005feea4 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
@@ -53,6 +53,16 @@ lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} :
         [⟨-1, (dya n).length, -1, by omega⟩].get) := by
   sorry
 
+@[simp, grind =]
+lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
+  (succ i).spaceUsed_list tapes sorry = 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
 
 end Routines
 
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean b/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean
index a4d97db5..cde75f28 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean
@@ -9,6 +9,7 @@ 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
 
@@ -69,6 +70,13 @@ public def MultiTapeTM.with_tapes {k₁ k₂ : ℕ}
   (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₁ α) (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.
 
 /--
@@ -111,6 +119,21 @@ 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₂ : ℕ}
@@ -123,4 +146,5 @@ public theorem MultiTapeTM.with_tapes_eval
   sorry
 
 
+
 end Turing

From cfc4ec77e76a4ccc894f90ba0728d1867d9c66b9 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 4 Mar 2026 13:16:13 +0100
Subject: [PATCH 2/4] space proofs

---
 .../Machines/MultiTapeTuring/AddRoutine.lean  | 63 ++++++++++++++--
 .../MultiTapeTuring/ListEncoding.lean         |  4 +-
 .../MultiTapeTuring/LoopCombinator.lean       | 74 +++++++++++++++++--
 .../Machines/MultiTapeTuring/SuccRoutine.lean | 26 +++++++
 4 files changed, 154 insertions(+), 13 deletions(-)

diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
index 0afa4143..78737b86 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,16 +53,65 @@ 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
+
+
+private lemma succ_space_at_iter {k : ℕ} (i j : Fin k)
+    (h_halts : ∀ tapes, (succ i).haltsOn tapes)
+    (n : ℕ) (tapes : Fin k → List (List OneTwo)) :
+    (space_at_iter h_halts n tapes) j =
+      if j = i then (listToString (((succ i).eval_list tapes).get (by sorry) j)).length
+      else spaceUsed_init tapes j := 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 => 1 + spaceUsed_init tapes 0
+    | 0 => spaceUsed_init tapes 0
     | 1 => 1 + spaceUsed_init tapes 1
-    | 2 => 1 + ((dya (dya_inv ((tapes 2).headD [])).succ) :: (tapes 2).tail).length
-    | 3 => 1 + ((tapes 3).headD []).length + spaceUsed_init tapes 3
-    | 4 => 1 + ((tapes 4).headD []).length + spaceUsed_init tapes 4
-    | 5 => 1 + ((tapes 5).headD []).length + spaceUsed_init tapes 5 := by
-  sorry
+    | 2 => max (((tapes 1).headD []).length + 1 + spaceUsed_init tapes 2)
+               ((dya (dya_inv ((tapes 1).headD [])).succ).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
+  -- 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
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
index 16f3a951..b8c4173b 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
@@ -168,10 +168,12 @@ public noncomputable def MultiTapeTM.spaceUsed_list
     (h_halts : ∀ tapes, tm.haltsOn tapes := by simp) : Fin k → ℕ := sorry
 
 /-- The space initially used by a Turing machine that has the given tape configuration. -/
-@[simp] -- TODO do we need simp here?
 public def spaceUsed_init (tapes : Fin k → List (List α)) : Fin k → ℕ := fun i =>
   (listToString (tapes i)).length
 
+public def spaceUsed_init_simp (tapes : Fin k → List (List α)) (i : Fin k) :
+  spaceUsed_init tapes i = (listToString (tapes i)).length := by simp [spaceUsed_init]
+
 -- 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
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
index 1d30d192..fd19bbbd 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
@@ -69,21 +69,83 @@ public noncomputable def space_at_iter {k : ℕ}
       (tm.spaceUsed_list
         ((fun tapes => (tm.eval_list tapes).get (by sorry))^[iter] tapes) h_halts i)
 
+public theorem space_at_iter_of_mono {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (h_halts : ∀ tapes, tm.haltsOn tapes)
+  (h_mono : sorry)
+  (iteration : ℕ)
+  (tapes : Fin k → List (List OneTwo))
+  (i : Fin k) :
+  space_at_iter h_halts iteration.succ tapes = tm.spaceUsed_list
+      ((fun tapes => (tm.eval_list tapes).get (by sorry))^[iteration] tapes) h_halts i := by
+  sorry
+
 -- TODO the following is probably not true for aux tapes. There we might need a bound.
 
+public noncomputable def output_length {k : ℕ}
+  (tm : MultiTapeTM k (WithSep OneTwo))
+  (tapes : Fin k → List (List OneTwo))
+  (i : Fin k) : Part ℕ :=
+  (tm.eval_list tapes).map fun t => (listToString (t i)).length
+
+public lemma output_length_value {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  (tapes : Fin k → List (List OneTwo))
+  (i : Fin k) :
+  output_length tm tapes i = (tm.eval_list tapes).map fun t => (listToString (t i)).length := by
+  simp [output_length]
+
+public def output_length_mono {k : ℕ}
+  (tm : MultiTapeTM k (WithSep OneTwo))
+  (i : Fin k) : Prop :=
+  ∀ tapes, ((output_length tm tapes i).map
+    fun len => len ≥ (listToString (tapes i)).length) = .some true
+
+public lemma output_length_mono_iff {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  {i : Fin k} :
+  output_length_mono tm i ↔ ∀ tapes, (output_length tm tapes i).map
+    fun len => len ≥ (listToString (tapes i)).length = .some true := by
+  simp [output_length_mono]
+
+public def space_use_is_output_length {k : ℕ}
+  (tm : MultiTapeTM k (WithSep OneTwo))
+  (i : Fin k) : Prop :=
+  ∀ tapes, (.some (tm.spaceUsed_list tapes sorry i) = output_length tm tapes i)
+
+public lemma space_use_is_output_length_iff {k : ℕ}
+  {tm : MultiTapeTM k (WithSep OneTwo)}
+  {i : Fin k} :
+  space_use_is_output_length tm i ↔
+    ∀ tapes, (.some (tm.spaceUsed_list tapes sorry i) = output_length tm tapes i) := by
+  simp [space_use_is_output_length]
+
+-- TODO this still does not work, it only works if it only depends on the length.
+public def space_use_mono {k : ℕ}
+  (tm : MultiTapeTM k (WithSep OneTwo))
+  (i : Fin k) : Prop :=
+  ∀ tapes, (listToString (tapes i)).length ≤ (tm.spaceUsed_list tapes sorry i)
+
+public lemma space_use_mono_iff {k : ℕ}
+  (tm : MultiTapeTM k (WithSep OneTwo))
+  (i : Fin k) :
+  space_use_mono tm i ↔
+    ∀ tapes, (listToString (tapes i)).length ≤ (tm.spaceUsed_list tapes sorry i) := by
+  simp [space_use_mono]
+
 @[simp]
 public lemma space_at_iter_of_mono {k : ℕ}
   {tm : MultiTapeTM k (WithSep OneTwo)}
   (h_halts : ∀ tapes, tm.haltsOn tapes)
   (i : Fin k)
-  -- The machine does not delete anything on the tape.
-  (h_mono_output : ∀ tapes, (tapes i).length ≤ ((tm.eval_list tapes).get (by sorry) i).length)
-  -- The machine does not have any exess space usage
-  (h_mono_space : ∀ tapes, (spaceUsed_init tapes i) =
-      ((tm.eval_list tapes).get (by sorry) i).length)
+  -- The machine's output on tape i is at least as large as the input.
+  (h_mono_output : output_length_mono tm i)
+  -- The machine's space use is the same as the output length.
+  (h_mono_space : space_use_is_output_length tm i)
   (iteration : ℕ)
   (tapes : Fin k → List (List OneTwo)) :
-  space_at_iter h_halts iteration tapes i = ((tm.eval_list tapes).get (by sorry) i).length := by
+  space_at_iter h_halts iteration tapes i =
+    (((Part.bind · tm.eval_list)^[iteration] tapes).get sorry i).length := by
   sorry
 
 @[simp]
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
index 005feea4..c8f4c619 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
 
@@ -36,6 +37,10 @@ Pushes zero if the tape is empty. -/
 public def succ {k : ℕ} (i : Fin k) : MultiTapeTM k (WithSep OneTwo) :=
   succ₀.with_tapes [i].get (by intro x y; grind)
 
+@[simp]
+public theorem succ_halts {k : ℕ} {i : Fin k} : ∀ tapes, (succ i).haltsOn tapes := by
+  sorry
+
 @[simp]
 public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
   (succ i).eval_list tapes = .some (Function.update tapes i
@@ -64,6 +69,27 @@ lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)
   --     2 + (listToString (tapes i)).length) -- We need to move at least one char to the left
   -- := by sorry
 
+@[simp]
+lemma succ_output_length_mono {k : ℕ} {i j : Fin k} : output_length_mono (succ i) j := by
+  apply output_length_mono_iff.mpr
+  intro tapes
+  simp [output_length_value]
+  sorry
+
+@[simp]
+lemma succ_space_use_is_output_length {k : ℕ} {i j : Fin k} :
+    space_use_is_output_length (succ i) j := by
+  apply space_use_is_output_length_iff.mpr
+  intro tapes
+  simp [output_length_value]
+
+  -- TODO this is actually wrong!
+
+
+
+
+  sorry
+
 end Routines
 
 end Turing

From f9217f64774eaac40bd5d9d87290f1a39727fe30 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 4 Mar 2026 13:42:37 +0100
Subject: [PATCH 3/4] space iter

---
 .../Machines/MultiTapeTuring/AddRoutine.lean  |  6 ++----
 .../MultiTapeTuring/ListEncoding.lean         |  8 ++++++++
 .../MultiTapeTuring/LoopCombinator.lean       | 20 ++++++++++++-------
 .../Machines/MultiTapeTuring/SuccRoutine.lean |  7 +++++++
 4 files changed, 30 insertions(+), 11 deletions(-)

diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
index 78737b86..a29db673 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
@@ -63,11 +63,9 @@ private lemma succ_eval_list_get_apply {k : ℕ} {i j : Fin k}
 
 
 private lemma succ_space_at_iter {k : ℕ} (i j : Fin k)
-    (h_halts : ∀ tapes, (succ i).haltsOn tapes)
     (n : ℕ) (tapes : Fin k → List (List OneTwo)) :
-    (space_at_iter h_halts n tapes) j =
-      if j = i then (listToString (((succ i).eval_list tapes).get (by sorry) j)).length
-      else spaceUsed_init tapes j := by
+  space_at_iter (tm := succ i) succ_halts n tapes j = Function.update (spaceUsed_init tapes)
+      i (listToString (((succ i).eval_list tapes).get (by sorry) j)).length := by
   sorry
 
 theorem add₀_spaceUsed {tapes : Fin 6 → List (List OneTwo)} :
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
index b8c4173b..8b601bd0 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean
@@ -174,6 +174,14 @@ public def spaceUsed_init (tapes : Fin k → List (List α)) : Fin k → ℕ :=
 public def spaceUsed_init_simp (tapes : Fin k → List (List α)) (i : Fin k) :
   spaceUsed_init tapes i = (listToString (tapes i)).length := by simp [spaceUsed_init]
 
+@[simp]
+public lemma spaceUsed_init_le_spaceUsed {k : ℕ} {α : Type}
+  {tm : MultiTapeTM k (WithSep α)}
+  (tapes : Fin k → List (List α))
+  (i : Fin k) :
+  spaceUsed_init tapes i ≤ MultiTapeTM.spaceUsed_list tm tapes sorry 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
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
index fd19bbbd..206476cb 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
@@ -72,13 +72,19 @@ public noncomputable def space_at_iter {k : ℕ}
 public theorem space_at_iter_of_mono {k : ℕ}
   {tm : MultiTapeTM k (WithSep OneTwo)}
   (h_halts : ∀ tapes, tm.haltsOn tapes)
-  (h_mono : sorry)
+  (i : Fin k)
+  (h_mono_step : ∀ tapes, tm.spaceUsed_list tapes h_halts i ≤
+     tm.spaceUsed_list ((tm.eval_list tapes).get sorry) h_halts i)
   (iteration : ℕ)
-  (tapes : Fin k → List (List OneTwo))
-  (i : Fin k) :
-  space_at_iter h_halts iteration.succ tapes = tm.spaceUsed_list
-      ((fun tapes => (tm.eval_list tapes).get (by sorry))^[iteration] tapes) h_halts i := by
-  sorry
+  (tapes : Fin k → List (List OneTwo)) :
+  space_at_iter h_halts iteration.succ tapes i = tm.spaceUsed_list
+      ((fun tapes => (tm.eval_list tapes).get sorry)^[iteration] tapes) h_halts i := by
+  induction iteration generalizing tapes with
+  | zero => simp [space_at_iter]
+  | succ iter ih =>
+    unfold space_at_iter
+    rw [ih]
+    simp only [Function.iterate_succ', Function.comp_apply, sup_eq_right, h_mono_step]
 
 -- TODO the following is probably not true for aux tapes. There we might need a bound.
 
@@ -134,7 +140,7 @@ public lemma space_use_mono_iff {k : ℕ}
   simp [space_use_mono]
 
 @[simp]
-public lemma space_at_iter_of_mono {k : ℕ}
+public lemma space_at_iter_of_mono' {k : ℕ}
   {tm : MultiTapeTM k (WithSep OneTwo)}
   (h_halts : ∀ tapes, tm.haltsOn tapes)
   (i : Fin k)
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
index c8f4c619..dd3d1eda 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
@@ -69,6 +69,13 @@ lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)
   --     2 + (listToString (tapes i)).length) -- We need to move at least one char to the left
   -- := by sorry
 
+@[simp]
+lemma succ_spaceUsed_mono_iter {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
+  (succ i).spaceUsed_list tapes (by simp) i ≤
+    (succ i).spaceUsed_list (((succ i).eval_list tapes).get (by simp)) succ_halts i := by
+  simp
+
+
 @[simp]
 lemma succ_output_length_mono {k : ℕ} {i j : Fin k} : output_length_mono (succ i) j := by
   apply output_length_mono_iff.mpr

From 3d6f785bfd41343d512161185fb24880aed07e3e Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 4 Mar 2026 14:13:04 +0100
Subject: [PATCH 4/4] more loops

---
 .../Machines/MultiTapeTuring/AddRoutine.lean  | 96 ++++++++++++-------
 .../MultiTapeTuring/LoopCombinator.lean       | 20 ++++
 .../Machines/MultiTapeTuring/SuccRoutine.lean | 27 +-----
 3 files changed, 83 insertions(+), 60 deletions(-)

diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
index a29db673..38a4cc0a 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean
@@ -62,11 +62,20 @@ private lemma succ_eval_list_get_apply {k : ℕ} {i j : Fin k}
   sorry
 
 
-private lemma succ_space_at_iter {k : ℕ} (i j : Fin k)
+private lemma succ_space_at_iter {k : ℕ} (i : Fin k)
     (n : ℕ) (tapes : Fin k → List (List OneTwo)) :
-  space_at_iter (tm := succ i) succ_halts n tapes j = Function.update (spaceUsed_init tapes)
-      i (listToString (((succ i).eval_list tapes).get (by sorry) j)).length := by
-  sorry
+  space_at_iter (tm := succ i) succ_halts n.succ tapes = Function.update (spaceUsed_init tapes)
+      i 1 + (listToString (((succ i).eval_list tapes).get (by sorry) i)).length := by
+  funext j
+  by_cases h : j = i
+  · rw [h, space_at_iter_of_mono succ_halts]
+    · simp
+      sorry
+    · intro tapes
+      exact succ_spaceUsed_mono_iter
+  · simp [h]
+    sorry
+
 
 theorem add₀_spaceUsed {tapes : Fin 6 → List (List OneTwo)} :
   add₀.spaceUsed_list tapes (h_halts := by sorry) = fun j : Fin 6 =>
@@ -78,38 +87,53 @@ theorem add₀_spaceUsed {tapes : Fin 6 → List (List OneTwo)} :
     | 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
-  -- 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]
+  simp [add₀, copy_halts, succ_halts, loop_halts_of_halts]
+  funext j
+  match j with
+  | 0 => simp
+         rw [space_at_iter_of_constant]
+         · sorry
+         · simp
+           sorry
+         · simp
+  | 1 => sorry
+  | 2 => 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
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
index 206476cb..25bda90a 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean
@@ -50,6 +50,7 @@ public theorem loop_eval_list {i : ℕ} {h_i : i < k}
           fun tapes' => tapes_extend_by tapes' tapes := by
   sorry
 
+@[simp]
 public theorem loop_halts_of_halts
   {i : ℕ} {h_i : i < k}
   {tm : MultiTapeTM k (WithSep OneTwo)}
@@ -86,6 +87,25 @@ public theorem space_at_iter_of_mono {k : ℕ}
     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.haltsOn tapes}
+  {i : Fin k}
+  (h_constant_space : ∀ tapes, tm.spaceUsed_list tapes h_halts 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
+
 -- TODO the following is probably not true for aux tapes. There we might need a bound.
 
 public noncomputable def output_length {k : ℕ}
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
index dd3d1eda..756d658e 100644
--- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
+++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean
@@ -59,9 +59,9 @@ lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} :
   sorry
 
 @[simp, grind =]
-lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
+public lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
   (succ i).spaceUsed_list tapes sorry = Function.update (spaceUsed_init tapes) i
-    1 + ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail).length := by
+    (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.
@@ -70,33 +70,12 @@ lemma succ_spaceUsed {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)
   -- := by sorry
 
 @[simp]
-lemma succ_spaceUsed_mono_iter {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
+public lemma succ_spaceUsed_mono_iter {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} :
   (succ i).spaceUsed_list tapes (by simp) i ≤
     (succ i).spaceUsed_list (((succ i).eval_list tapes).get (by simp)) succ_halts i := by
   simp
 
 
-@[simp]
-lemma succ_output_length_mono {k : ℕ} {i j : Fin k} : output_length_mono (succ i) j := by
-  apply output_length_mono_iff.mpr
-  intro tapes
-  simp [output_length_value]
-  sorry
-
-@[simp]
-lemma succ_space_use_is_output_length {k : ℕ} {i j : Fin k} :
-    space_use_is_output_length (succ i) j := by
-  apply space_use_is_output_length_iff.mpr
-  intro tapes
-  simp [output_length_value]
-
-  -- TODO this is actually wrong!
-
-
-
-
-  sorry
-
 end Routines
 
 end Turing