diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
index 74303c236e..b23837b349 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -30,8 +30,8 @@ The results are layered, from the purely combinatorial to the machine-specific:
 * `MultiTapeTM.encard_fitsIn_le` is a counting statement about the type `Storage` alone and does
   not mention Turing machines: a memory whose non-blank cells and heads stay within per-tape
   windows of total size `s` can hold at most `storageBound Symbol State k s` different values.
-* `MultiTapeTM.storage_fitsIn` is the geometric input: the storage reached after `t` steps stays
-  within the windows given by the space used up to step `t`.
+* `MultiTapeNTM.ComputationPath.storage_fitsIn` is the geometric input: the storage at the end of a
+  computation path stays within the windows given by the per-tape space of the path.
 * `MultiTapeTM.encard_storages_le` combines the two: a machine bounded by space `s` passes through
   at most `storageBound Symbol State k s` storages *during its whole run*, no matter how long it
   runs and how long its input is. This is the form needed for arguments below logarithmic space,
@@ -62,8 +62,9 @@ alphabet exponent.
 We lose a factor of `2 * k` by simplifying the windows to `[-sᵢ, sᵢ]` instead of the actually used
 area, but this is absorbed by the `O(s)` exponent in the final bound.
 
-The windows for a whole run are available because a machine that is space-bounded at every point in
-time attains its per-tape space usage at a single step (`MultiTapeTM.exists_spaceUsedByTape_max`).
+The windows for a whole run are available because the computation paths of a deterministic
+machine are prefixes of one another, so the one visiting the most cells contains the windows of
+every other (`MultiTapeNTM.ComputationPath.spaceUsedByTape_le_of_space_le`).
 -/
 
 @[expose] public section
@@ -247,63 +248,58 @@ def Cfg.core (c : Cfg k Symbol State input) :
     Fin (input.length + 2) × Storage Symbol State k :=
   (c.inputPos, c.storage)
 
-/-- `step` never reads the output tape, so the core of the next configuration is determined by the
-core of the current one. -/
-lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) :
-    (tm.step c₁).core = (tm.step c₂).core := by
-  rcases c₁ with ⟨q₁, i₁, w₁, p₁, out₁⟩
-  rcases c₂ with ⟨q₂, i₂, w₂, p₂, out₂⟩
-  simp only [Cfg.core, Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h
-  obtain ⟨rfl, rfl, rfl, rfl⟩ := h
-  cases q₁ with
-  | none => rw [MultiTapeTM.step_of_halt rfl, MultiTapeTM.step_of_halt rfl]; rfl
-  | some q => rw [MultiTapeTM.step_of_state rfl, MultiTapeTM.step_of_state rfl]; rfl
-
 /-! ## The storages and cores of a space-bounded run
 
 These are the main results giving upper bounds on the number of storages and configuration cores
 reachable in bounded space.
 -/
 
-namespace MultiTapeTM
+namespace MultiTapeNTM
 
-/-- The storage reached after `t` steps fits in the windows given by the per-tape space usage up
-to step `t`. -/
-lemma storage_fitsIn (t : ℕ) :
-    (tm.runFrom (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) t) := by
-  constructor
-  · intro j
-    simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited
-      (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)
-  · intro j
-    exact content_natAbs_le_spaceUsedByTape t
+/-- The storage at the end of a computation path fits in the windows given by its per-tape space:
+the tapes start blank, with every head at `0`. -/
+lemma ComputationPath.storage_fitsIn {ntm : MultiTapeNTM k Symbol State}
+    (p : ntm.ComputationPath input) : p.last.storage.FitsIn p.spaceUsedByTape := by
+  refine ⟨fun j => ?_, fun j z hz => ?_⟩
+  · simpa [Cfg.storage, p.head_eq, Cfg.init, ComputationPath.spaceUsedByTape] using
+      RunPath.natAbs_le_spaceUsedByTape_of_mem_visited p.toRunPath
+        ((RunPath.mem_visitedByTapeHead _).mpr ⟨_, RelSeries.last_mem _, rfl⟩)
+  · simpa [p.head_eq, Cfg.init, ComputationPath.spaceUsedByTape] using
+      RunPath.natAbs_le_spaceUsedByTape_of_mem_visited p.toRunPath
+        (RunPath.mem_visitedByTapeHead_of_workTapes_ne _
+          (by simpa [p.head_eq, Cfg.init, Cfg.storage] using hz))
+
+end MultiTapeNTM
+
+namespace MultiTapeTM
 
 /-- A machine that uses at most `s` cells of work-tape space at every point in time passes through
 at most `storageBound Symbol State k s` different storages during its whole run — independently of
 the length of the input and of how long it runs. -/
 theorem encard_storages_le [Fintype Symbol] [Fintype State] {s : ℕ}
-    (hs : ∀ t, tm.space (tm.initCfg input) t ≤ s) :
-    (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard
+    (hs : tm.RunsInSpace input s) :
+    (Set.range fun p : tm.ComputationPath input => p.last.storage).encard
       ≤ storageBound Symbol State k s := by
-  obtain ⟨T, hT⟩ := tm.exists_spaceUsedByTape_max (tm.initCfg input) hs
-  refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs T))
-  rintro _ ⟨t, rfl⟩
-  exact Storage.FitsIn_mono (fun i => hT t i) (tm.storage_fitsIn t)
+  -- every storage fits in the windows of a computation path visiting the most cells
+  obtain ⟨p, hp⟩ := hs.exists_space_max
+  refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs p))
+  rintro _ ⟨q, rfl⟩
+  exact Storage.FitsIn_mono (q.spaceUsedByTape_le_of_space_le (hp q)) q.storage_fitsIn
 
 /-- The number of configuration cores that a machine bounded by space `s` can reach is at most
 `(n + 2) * storageBound Symbol State k s`, where `n` is the length of the input. -/
 theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
-    (hs : ∀ t, tm.space (tm.initCfg input) t ≤ s) :
-    (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+    (hs : tm.RunsInSpace input s) :
+    (Set.range fun p : tm.ComputationPath input => p.last.core).encard
       ≤ (input.length + 2) * storageBound Symbol State k s := by
-  calc (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+  calc (Set.range fun p : tm.ComputationPath input => p.last.core).encard
       ≤ ((Set.univ : Set (Fin (input.length + 2)))
-          ×ˢ (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage)).encard := by
+          ×ˢ (Set.range fun p : tm.ComputationPath input => p.last.storage)).encard := by
         apply Set.encard_le_encard
-        rintro _ ⟨t, rfl⟩
-        exact ⟨Set.mem_univ _, t, rfl⟩
+        rintro _ ⟨p, rfl⟩
+        exact ⟨Set.mem_univ _, p, rfl⟩
     _ = (Set.univ : Set (Fin (input.length + 2))).encard
-          * (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard := Set.encard_prod
+          * (Set.range fun p : tm.ComputationPath input => p.last.storage).encard := Set.encard_prod
     _ ≤ (input.length + 2) * storageBound Symbol State k s := by
         refine mul_le_mul' ?_ (tm.encard_storages_le hs)
         simp [Set.encard_univ, ENat.card_eq_coe_fintype_card]
@@ -312,8 +308,8 @@ theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
 passes through is at most `2 ^ (O(s))`, with constants depending only on the machine. -/
 theorem encard_storages_le_pow [Finite Symbol] [Finite State] :
     ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
-      (∀ t, tm.space (tm.initCfg input) t ≤ s) →
-      (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard ≤ a * 2 ^ (c * s) := by
+      tm.RunsInSpace input s →
+      (Set.range fun p : tm.ComputationPath input => p.last.storage).encard ≤ a * 2 ^ (c * s) := by
   have : Fintype Symbol := Fintype.ofFinite Symbol
   have : Fintype State := Fintype.ofFinite State
   obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)
@@ -325,8 +321,8 @@ is at most `(n + 2) * 2 ^ (O(s))`, with constants depending only on the machine
 input. -/
 theorem encard_cores_le_pow [Finite Symbol] [Finite State] :
     ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
-      (∀ t, tm.space (tm.initCfg input) t ≤ s) →
-      (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+      tm.RunsInSpace input s →
+      (Set.range fun p : tm.ComputationPath input => p.last.core).encard
         ≤ (input.length + 2) * a * 2 ^ (c * s) := by
   have : Fintype Symbol := Fintype.ofFinite Symbol
   have : Fintype State := Fintype.ofFinite State
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 84db17a4fe..33afcdebb2 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
@@ -34,7 +34,6 @@ We define a number of structures and concepts related to multi-tape Turing machi
 * `step`, `runFrom`: the successor configuration and iteration of this function
 * `MultiTapeNTM.RunPath.ofDeterministic`, `MultiTapeNTM.ComputationPath.ofDeterministic`:
     paths of a given length from an arbitrary or initial configuration
-* `space`: the space of the path of the first `t` steps from a configuration
 * `Computes`: the machine halts with the given output on an input
 * `ComputesInTimeAndSpace`: the machine produces an output within the shared resource bounds
 * `ComputesFunInTimeAndSpace`: function computation with the shared time and space bounds
@@ -225,6 +224,32 @@ lemma ComputationPath.eq_ofDeterministic (p : tm.ComputationPath input) :
   congr 1
   exact (RunPath.eq_ofDeterministic p).trans (by rw [hp]; rfl)
 
+/-- Deterministic run paths from the same configuration are prefixes of one another: the shorter one
+is the longer one, cut at its length. -/
+lemma RunPath.eq_take {p q : tm.RunPath input} (hhead : p.head = q.head) (h : p.length ≤ q.length) :
+    p = q.take ⟨p.length, Nat.lt_succ_of_le h⟩ := by
+  refine p.eq_ofDeterministic.trans ((eq_ofDeterministic (q.take _)).trans ?_).symm
+  rw [RelSeries.head_take, hhead]
+  rfl
+
+/-- The computation paths of a deterministic machine are prefixes of one another, so a path visiting
+at most as many cells as another visits at most as many on each tape. -/
+lemma ComputationPath.spaceUsedByTape_le_of_space_le (p : tm.ComputationPath input)
+    {q : tm.ComputationPath input} (h : p.space ≤ q.space) :
+    p.spaceUsedByTape ≤ q.spaceUsedByTape := by
+  -- a shorter path is a prefix of a longer one, so it visits fewer cells on each tape
+  have hmono {p q : tm.ComputationPath input} (h : p.time ≤ q.time) :
+      p.spaceUsedByTape ≤ q.spaceUsedByTape := fun i => by
+    change RunPath.spaceUsedByTape p.toRunPath i ≤ RunPath.spaceUsedByTape q.toRunPath i
+    rw [RunPath.eq_take (by rw [p.head_eq, q.head_eq]) h]
+    exact Finset.card_le_card (RunPath.visitedByTapeHead_take_subset _ _ i)
+  rcases le_total p.time q.time with hpq | hqp
+  · exact hmono hpq
+  -- a longer `p` visits no more cells than `q`, so it visits exactly those of `q`
+  have h : ∑ j, p.spaceUsedByTape j ≤ ∑ j, q.spaceUsedByTape j := h
+  exact fun i => ((Finset.sum_eq_sum_iff_of_le fun j _ => hmono hqp j).mp
+    (le_antisymm (Finset.sum_le_sum fun j _ => hmono hqp j) h) i (Finset.mem_univ i)).ge
+
 /-- A step-preserving map sends the path of `t` steps from `cfg` to the path of `t` steps from the
 image of `cfg`. -/
 lemma RunPath.map_ofDeterministic {k' : ℕ} {State' : Type*} {input' : List Symbol}
@@ -281,48 +306,6 @@ lemma runsInTime_of_halted {input : List Symbol} {t : ℕ}
   rw [computationPath_last_eq_runFrom p, runFrom_eq_of_halt _ _ hp h]
   exact h
 
-/-- The work-tape head moves by at most one cell in a single step. -/
-lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) :
-    |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by
-  cases hstate : c.state with
-  | none => simp [step_of_halt hstate]
-  | some q => rw [step_of_state hstate]; exact workTapePos_apply_le _ c i
-
-section Space
-/-! Now we define space usage and add some helper lemmas. -/
-
-/-- The set of positions visited by the head of work tape `i` in the computation starting from
-configuration `cfg` up to step `t`. -/
-noncomputable def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    Finset ℤ :=
-  Finset.univ.image fun n : Fin (t + 1) => (tm.runFrom cfg n).workTapePos i
-
-/--
-The number of work tape cells visited by the head of tape `i` in the computation starting from
-configuration `cfg` up to step `t`.
--/
-noncomputable def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ :=
-  (tm.visitedByTapeHead cfg t i).card
-
-/-- The number of work tape cells visited in the first `t` steps from `cfg`: the space of the path
-of these steps. -/
-noncomputable abbrev space (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ :=
-  (MultiTapeNTM.RunPath.ofDeterministic tm cfg t).space
-
-/-- A zero-tape Turing machine uses zero space. -/
-@[simp]
-lemma space_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) :
-    tm.space cfg t = 0 := by
-  subst h_zero
-  simp [MultiTapeNTM.RunPath.space]
-
-/-- Each tape's space usage is bounded by the total space used. -/
-lemma spaceUsedByTape_le_space (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    tm.spaceUsedByTape cfg t i ≤ tm.space cfg t :=
-  Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)
-
-end Space
-
 /-- In `t` steps the input head moves at most `t` positions to the right. -/
 lemma inputPos_runFrom_le (tm : MultiTapeTM k Symbol State)
     (cfg : Cfg k Symbol State input) (t : ℕ) :
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Space.lean b/Cslib/Computability/Machines/Turing/MultiTape/Space.lean
index e119511cb6..330a56806c 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Space.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Space.lean
@@ -8,6 +8,7 @@ module
 
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Data.Int.Interval
+public import Mathlib.Order.Lattice.Nat
 public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
 
 /-!
@@ -98,6 +99,25 @@ lemma space_le_of_subset {p q : ntm.RunPath input} (h : ∀ c ∈ q, c ∈ p) :
     let ⟨n, hn⟩ := h c hc
     hn ▸ Finset.mem_image_of_mem _ (Finset.mem_univ n)
 
+/-- A path visits exactly the head positions of its configurations. -/
+@[simp]
+lemma mem_visitedByTapeHead (p : ntm.RunPath input) {i : Fin k} {z : ℤ} :
+    z ∈ p.visitedByTapeHead i ↔ ∃ c ∈ p, c.workTapePos i = z := by
+  simp [visitedByTapeHead, RelSeries.mem_def]
+
+/-- A prefix of a path visits only cells that the path visits. -/
+lemma visitedByTapeHead_take_subset (p : ntm.RunPath input) (j : Fin (p.length + 1)) (i : Fin k) :
+    visitedByTapeHead (p.take j) i ⊆ p.visitedByTapeHead i :=
+  Finset.image_subset_iff.mpr fun n _ =>
+    p.mem_visitedByTapeHead.mpr ⟨_, ⟨Fin.castLE j.isLt n, rfl⟩, rfl⟩
+
+/-- Extending a path by a configuration visits its head positions as well. -/
+lemma visitedByTapeHead_snoc (p : ntm.RunPath input) (c : Cfg k Symbol State input)
+    (h : ntm.Step p.last c) (i : Fin k) :
+    visitedByTapeHead (p.snoc c h) i = insert (c.workTapePos i) (p.visitedByTapeHead i) := by
+  ext z
+  simp [RelSeries.mem_snoc, or_and_right, exists_or, eq_comm, or_comm]
+
 /-! ### Windows -/
 
 /-- Every head stays within the window `[-s, s]` along the path. -/
@@ -140,6 +160,10 @@ lemma space_map_le (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.st
 
 end RunPath
 
+/-- The number of positions visited by the head of work tape `i` along a computation path. -/
+def ComputationPath.spaceUsedByTape (p : ntm.ComputationPath input) (i : Fin k) : ℕ :=
+  RunPath.spaceUsedByTape p.toRunPath i
+
 /-- The number of work tape cells visited along a computation path. -/
 def ComputationPath.space (p : ntm.ComputationPath input) : ℕ := RunPath.space p.toRunPath
 
@@ -153,6 +177,16 @@ lemma RunsInSpace.mono {s s' : ℕ} (h : ntm.RunsInSpace input s) (hs : s ≤ s'
     ntm.RunsInSpace input s' :=
   fun p ↦ (h p).trans hs
 
+/-- A machine running in space `s` has a computation path visiting the most cells. -/
+lemma RunsInSpace.exists_space_max {s : ℕ} (hs : ntm.RunsInSpace input s) :
+    ∃ p : ntm.ComputationPath input, ∀ q : ntm.ComputationPath input, q.space ≤ p.space := by
+  have hne : (Set.range fun p : ntm.ComputationPath input => p.space).Nonempty :=
+    ⟨_, ⟨.singleton _ (ntm.initCfg input), rfl⟩, rfl⟩
+  have hbdd : BddAbove (Set.range fun p : ntm.ComputationPath input => p.space) :=
+    ⟨s, by rintro _ ⟨p, rfl⟩; exact hs p⟩
+  obtain ⟨p, hp⟩ := Nat.sSup_mem hne hbdd
+  exact ⟨p, fun q => (le_csSup hbdd ⟨q, rfl⟩).trans_eq hp.symm⟩
+
 /-- A machine without work tapes satisfies every space bound. -/
 @[simp]
 lemma runsInSpace_zero_tapes (ntm : MultiTapeNTM 0 Symbol State) (input : List Symbol) (s : ℕ) :
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
index c7f2241f04..d38e77461c 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
@@ -11,169 +11,94 @@ public import Mathlib.Data.Int.Interval
 public import Mathlib.Order.Lattice.Nat
 
 /-!
-# Tape head visitation and space-usage lemmas
+# Head movement along run paths
 
-This file collects lemmas about the set of positions visited by a work-tape head
-(`MultiTapeTM.visitedByTapeHead`) and the resulting space-usage measures
-(`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.space`) and how the tape head positions
-influence the cells that are modified on a tape.
-
-`MultiTapeTM.exists_spaceUsedByTape_max` shows that a computation whose space usage is bounded
-attains its per-tape space usage at a single step, which makes a bound that holds at every point
-in time usable as a bound for the whole run.
+This file collects how a step moves the work-tape heads and changes the work tapes, and what this
+implies for the cells visited along a run path: a head moves by at most one cell per step, so it
+visits every cell between its first and last positions, and a cell changes only under its head.
 
 -/
 
 @[expose] public section
 
-namespace Turing.MultiTapeTM
-
-variable {k : ℕ}
-variable {State Symbol : Type*}
-variable {input : List Symbol}
-variable {tm : MultiTapeTM k Symbol State}
-variable {cfg : Cfg k Symbol State input}
-
-/-- If the work tape head is not at position `z`, then the tape does not change there. -/
-lemma step_workTapes_eq_of_ne
-    (cfg : Cfg k Symbol State input)
-    (j : Fin k)
-    (z : ℤ)
-    (hz : z ≠ cfg.workTapePos j) :
-    (tm.step cfg).workTapes j z = cfg.workTapes j z := by
-  cases hst : cfg.state with
-  | none => simp [step_of_halt hst]
-  | some q =>
-    rw [step_of_state hst, Action.apply_workTapes]
-    rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes j).1 <;> simp_all
-
-lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} :
-    z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by
-  simp [visitedByTapeHead, Fin.exists_iff]
-
-lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    (tm.runFrom cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i :=
-  tm.mem_visitedByTapeHead.mpr ⟨t, by omega, rfl⟩
-
-/-- The set of positions visited by a tape head is monotone in the number of steps. -/
-lemma visitedByTapeHead_mono (cfg : Cfg k Symbol State input) (i : Fin k) {t t' : ℕ} (h : t ≤ t') :
-    tm.visitedByTapeHead cfg t i ⊆ tm.visitedByTapeHead cfg t' i := by
-  intro z hz
-  obtain ⟨n, hn, hz⟩ := tm.mem_visitedByTapeHead.mp hz
-  exact tm.mem_visitedByTapeHead.mpr ⟨n, by omega, hz⟩
-
-/-- Starting from configuration `cfg`, every position between the initial head position of tape
-`i` and the one after `t` steps is part of the "visited set" at step `t`. -/
-lemma uIcc_workTapePos_subset_visitedByTapeHead
-    (cfg : Cfg k Symbol State input) (i : Fin k) (t : ℕ) :
-    Finset.uIcc (cfg.workTapePos i) ((tm.runFrom cfg t).workTapePos i)
-      ⊆ tm.visitedByTapeHead cfg t i := by
-  induction t with
-  | zero => simpa [runFrom] using tm.mem_visitedByTapeHead_self cfg 0 i
-  | succ t ih =>
+namespace Turing.MultiTapeNTM
+
+variable {k k' : ℕ} {State State' Symbol : Type*} {input input' : List Symbol}
+variable {ntm : MultiTapeNTM k Symbol State} {ntm' : MultiTapeNTM k' Symbol State'}
+
+/-- A work-tape head moves by at most one cell in a single step. -/
+lemma Step.workTapePos_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) :
+    |c'.workTapePos i - c.workTapePos i| ≤ 1 := by
+  unfold Step at h
+  split at h
+  · simp [h]
+  · obtain ⟨a, _, rfl⟩ := h
+    exact workTapePos_apply_le a c i
+
+/-- A step does not change a work-tape cell away from its head. -/
+lemma Step.workTapes_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c c') {i : Fin k}
+    {z : ℤ} (hz : z ≠ c.workTapePos i) : c'.workTapes i z = c.workTapes i z := by
+  unfold Step at h
+  split at h
+  · simp [h]
+  · obtain ⟨a, _, rfl⟩ := h
+    rw [Action.apply_workTapes]
+    cases ha : (a.workTapes i).1 <;> simp [ha, hz]
+
+namespace RunPath
+
+/-- Every position between the first and the last position of a head along a path is visited,
+since the head moves by at most one cell per step. -/
+lemma uIcc_workTapePos_subset_visitedByTapeHead (p : ntm.RunPath input) (i : Fin k) :
+    Finset.uIcc (p.head.workTapePos i) (p.last.workTapePos i) ⊆ p.visitedByTapeHead i := by
+  induction p using RelSeries.inductionOn' with
+  | singleton c =>
+    simp +instances [visitedByTapeHead, RelSeries.singleton, RelSeries.head, RelSeries.last]
+  | snoc p c h ih =>
+    have hm := abs_le.mp (Step.workTapePos_le h i)
+    rw [RelSeries.head_snoc, RelSeries.last_snoc, visitedByTapeHead_snoc]
     intro z hz
-    have hstep :
-        |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 := by
-      simpa only [runFrom, Function.iterate_succ_apply'] using
-        tm.workTapePos_step_le (tm.runFrom cfg t) i
-    have hmono := tm.visitedByTapeHead_mono cfg i (Nat.le_succ t)
-    have hself := tm.mem_visitedByTapeHead_self cfg (t + 1) i
-    grind [Finset.mem_uIcc]
-
-/-- If a work tape cell is changed after `t` steps, it must have been visited by the tape head. -/
-lemma mem_visitedByTapeHead_of_workTapes_ne
-    (j : Fin k)
-    (t : ℕ)
-    (z : ℤ)
-    (h : (tm.runFrom cfg t).workTapes j z ≠ cfg.workTapes j z) :
-    z ∈ tm.visitedByTapeHead cfg t j := by
-  induction t with
-  | zero => exact absurd (by simp [runFrom]) h
-  | succ t ih =>
-    rw [runFrom, Function.iterate_succ_apply', ← runFrom] at h
-    by_cases hz : z = (tm.runFrom cfg t).workTapePos j
-    · exact hz ▸ tm.visitedByTapeHead_mono cfg j (Nat.le_succ t)
-        (tm.mem_visitedByTapeHead_self cfg t j)
-    · rw [tm.step_workTapes_eq_of_ne _ j z hz] at h
-      exact tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (ih h)
-
-/-- Every position visited by the head of tape `i` lies within `spaceUsedByTape … i` of the
-head's starting position. -/
-lemma natAbs_le_spaceUsedByTape_of_mem_visited
-    {i : Fin k}
-    {z : ℤ}
-    {t : ℕ}
-    (hz : z ∈ tm.visitedByTapeHead cfg t i) :
-    (z - cfg.workTapePos i).natAbs ≤ tm.spaceUsedByTape cfg t i := by
-  obtain ⟨t', ht', rfl⟩ := tm.mem_visitedByTapeHead.mp hz
-  have h1 := Finset.card_le_card
-    ((tm.uIcc_workTapePos_subset_visitedByTapeHead cfg i t').trans
-      (tm.visitedByTapeHead_mono cfg i (show t' ≤ t by omega)))
-  rw [Int.card_uIcc] at h1
-  unfold spaceUsedByTape
+    by_cases he : z = c.workTapePos i
+    · exact he ▸ Finset.mem_insert_self _ _
+    · exact Finset.mem_insert_of_mem (ih (by rw [Finset.mem_uIcc] at hz ⊢; omega))
+
+/-- A work-tape cell that differs between the first and the last configuration of a path was
+visited by its head. -/
+lemma mem_visitedByTapeHead_of_workTapes_ne (p : ntm.RunPath input) {i : Fin k} {z : ℤ}
+    (h : p.last.workTapes i z ≠ p.head.workTapes i z) : z ∈ p.visitedByTapeHead i := by
+  induction p using RelSeries.inductionOn' with
+  | singleton c => exact absurd rfl h
+  | snoc p c hs ih =>
+    rw [visitedByTapeHead_snoc]
+    refine Finset.mem_insert_of_mem ?_
+    by_cases hz : z = p.last.workTapePos i
+    · exact hz ▸ Finset.mem_image_of_mem _ (Finset.mem_univ (Fin.last _))
+    · rw [RelSeries.last_snoc, RelSeries.head_snoc, Step.workTapes_eq_of_ne hs hz] at h
+      exact ih h
+
+/-- Every position visited by a head lies within the space of its tape from its first position. -/
+lemma natAbs_le_spaceUsedByTape_of_mem_visited (p : ntm.RunPath input) {i : Fin k} {z : ℤ}
+    (hz : z ∈ p.visitedByTapeHead i) :
+    (z - p.head.workTapePos i).natAbs ≤ p.spaceUsedByTape i := by
+  obtain ⟨n, -, rfl⟩ := Finset.mem_image.mp hz
+  -- the prefix up to `n` visits every position between the first position and the one at `n`
+  have h := Finset.card_le_card
+    ((uIcc_workTapePos_subset_visitedByTapeHead (p.take n) i).trans
+      (p.visitedByTapeHead_take_subset n i))
+  rw [RelSeries.head_take, RelSeries.last_take, Int.card_uIcc] at h
+  change _ ≤ (p.visitedByTapeHead i).card
   omega
 
-/-- Every non-blank cell on work tape `i` lies within `spaceUsedByTape … i t` of the origin. -/
-lemma content_natAbs_le_spaceUsedByTape
-    {i : Fin k}
-    (t : ℕ)
-    (z : ℤ)
-    (h : (tm.runFrom (tm.initCfg input) t).workTapes i z ≠ none) :
-    z.natAbs ≤ tm.spaceUsedByTape (tm.initCfg input) t i := by
-  -- The work tapes start out blank, so any non-blank cell has been visited by the head; the
-  -- initial head position is `0`, so the displacement bound is a bound on the position itself.
-  simpa using tm.natAbs_le_spaceUsedByTape_of_mem_visited
-    (tm.mem_visitedByTapeHead_of_workTapes_ne i t z h)
-
-/-- The number of cells visited by a single work-tape head grows by at most one each step. -/
-lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    tm.spaceUsedByTape cfg t i ≤ t + 1 :=
-  Finset.card_image_le.trans_eq (by simp)
-
-/-- The space used by a computation is bounded linearly by the number of steps. -/
-lemma space_linear (cfg : Cfg k Symbol State input) (t : ℕ) :
-    tm.space cfg t ≤ k * t + k := by
-  calc tm.space cfg t
-      = ∑ i, (tm.spaceUsedByTape cfg t i) := by rfl
-    _ ≤ ∑ i, (t + 1) := Finset.sum_le_sum (fun i _ => tm.spaceUsedByTape_le cfg t i)
-    _ = k * t + k := by simp [Nat.mul_succ]
-
-/-- The space used by a single tape is monotone in the number of steps. -/
-lemma spaceUsedByTape_mono
-    (tm : MultiTapeTM k Symbol State)
-    (cfg : Cfg k Symbol State input)
-    (i : Fin k) :
-    Monotone (tm.spaceUsedByTape cfg · i) := by
-  intro t t' h
-  exact Finset.card_le_card (tm.visitedByTapeHead_mono cfg i h)
-
-/-- A computation whose total space usage stays below a bound reaches a step `T` at which the space
-usage of *every* tape is maximal. This turns a bound that holds at every point in time into a
-bound for the whole run. -/
-lemma exists_spaceUsedByTape_max (cfg : Cfg k Symbol State input) {s : ℕ}
-    (hs : ∀ t, tm.space cfg t ≤ s) :
-    ∃ T, ∀ t i, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg T i := by
-  -- The space usage of a single tape is bounded, so it attains its supremum at some step `T i`.
-  have h : ∀ i, ∃ Ti, ∀ t, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg Ti i := by
-    intro i
-    have hbdd : BddAbove (Set.range (tm.spaceUsedByTape cfg · i)) :=
-      ⟨s, by rintro _ ⟨t, rfl⟩; exact (tm.spaceUsedByTape_le_space cfg t i).trans (hs t)⟩
-    obtain ⟨Ti, hTi⟩ := Nat.sSup_mem (Set.range_nonempty (tm.spaceUsedByTape cfg · i)) hbdd
-    exact ⟨Ti, fun t => (le_csSup hbdd ⟨t, rfl⟩).trans hTi.ge⟩
-  choose T hT using h
-  -- Monotonicity lets us use a single step that is late enough for every tape.
-  exact ⟨Finset.univ.sup T, fun t i =>
-    (hT i t).trans (tm.spaceUsedByTape_mono cfg i (Finset.le_sup (Finset.mem_univ i)))⟩
-
-/-- A run path that starts with every head at cell `0` and visits at most `s` cells keeps its heads
+/-- A path that starts with every head at cell `0` and visits at most `s` cells keeps its heads
 within `[-s, s]`. -/
-lemma _root_.Turing.MultiTapeNTM.RunPath.inWindow_of_space_le {p : tm.RunPath input} {s : ℕ}
-    (h0 : ∀ i, p.head.workTapePos i = 0) (hs : p.space ≤ s) : p.InWindow s := by
-  rw [p.eq_ofDeterministic] at hs ⊢
-  rintro _ ⟨n, rfl⟩ i
-  have hz := tm.natAbs_le_spaceUsedByTape_of_mem_visited
-    ((tm.mem_visitedByTapeHead (cfg := p.head) (t := p.time) (i := i)).mpr ⟨n, n.2, rfl⟩)
+lemma inWindow_of_space_le {p : ntm.RunPath input} {s : ℕ} (h0 : ∀ i, p.head.workTapePos i = 0)
+    (hs : p.space ≤ s) : p.InWindow s := fun c hc i => by
+  have hz := p.natAbs_le_spaceUsedByTape_of_mem_visited
+    ((p.mem_visitedByTapeHead (i := i)).mpr ⟨c, hc, rfl⟩)
   rw [h0, sub_zero] at hz
-  exact mem_window.mpr (hz.trans ((tm.spaceUsedByTape_le_space _ _ i).trans hs))
+  exact mem_window.mpr <| hz.trans <|
+    (Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)).trans hs
+
+end RunPath
 
-end Turing.MultiTapeTM
+end Turing.MultiTapeNTM