diff --git a/Cslib.lean b/Cslib.lean
index a4d250711..81c530887 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -44,7 +44,10 @@ public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
 public import Cslib.Computability.Languages.SafetyLiveness
+public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean
new file mode 100644
index 000000000..27ea589ae
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean
@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Aviv Bar Natan
+-/
+
+module
+
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+public import Mathlib.Algebra.Order.Group.Abs
+public import Mathlib.Algebra.Order.Group.Int
+public import Mathlib.Data.Finset.Dedup
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Int.Interval
+public import Mathlib.Data.Sign.Defs
+public import Cslib.Init
+
+/-!
+# Configurations of Multi-Tape Turing Machines
+
+Configurations of a multi-tape Turing machine with a read-only input tape, `k` work tapes and one
+write-only output tape, together with what a single transition does to one and the space measure
+read off a list of them.
+
+## Design
+
+Nothing here mentions a machine. A step is described in two parts: an `Action`, recording
+which way the input head moves, what is written and where the work heads move, which symbol is
+emitted and which state follows; and `Action.apply`, which carries it out on a
+configuration.
+
+The output tape is part of the configuration, so the string emitted along a run can be read off
+the configuration the run ends in.
+
+## Important Declarations
+
+* `Cfg`: the configuration: the internal state, the tape contents and head positions, and the
+    output tape
+* `Action`: what a machine does in one step
+* `Action.apply`: the effect of one action on a configuration
+* `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in
+* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations
+-/
+
+@[expose] public section
+
+namespace Turing
+
+variable {k : ℕ} {State Symbol : Type*} {input : List Symbol}
+
+/-- What a machine does in one step. -/
+structure Action (k : ℕ) (Symbol State : Type*) where
+  /-- The movement (attempt) of the input head. -/
+  inputMove : SignType
+  /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/
+  workActions : Fin k → (Option (Option Symbol)) × SignType
+  /-- An optional symbol to output. -/
+  outS : Option Symbol
+  /-- The successor state or none to halt. -/
+  q' : Option State
+
+/--
+The configurations of a Turing machine is relative to the input of the machine and consist of:
+- an `Option`al state (or none for the halting state),
+- the position of the input head (shifted by one),
+- the contents of the work tape,
+- the positions of the work tape heads,
+- the contents of the write-only output tape
+-/
+@[ext]
+structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where
+  /-- the state of the TM (or none for the halting state) -/
+  state : Option State
+  /-- the position of the input head, shifted by one -/
+  inputPos : Fin (input.length + 2)
+  /-- the work tapes -/
+  workTapes : Fin k → ℤ → Option Symbol
+  /-- the positions of the heads on the work tapes -/
+  workTapePos : Fin k → ℤ
+  /-- the contents of the write-only output tape -/
+  output : List Symbol
+deriving Inhabited
+
+/-- Attempt to move the input tape head.
+The machine can only read one empty cell outside of the input,
+any attempted movement beyond that results in no movement.
+
+The addition is performed in `ℤ` before clamping. Performing it in `Fin (n + 2)` would wrap an
+outward boundary move to the opposite end of the input. -/
+@[scoped grind =]
+def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2) :=
+  let p := ((pos.val : ℤ) + (m.cast : ℤ)).toNat
+  if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩
+
+@[simp]
+lemma moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) :
+    moveInputPos pos 0 = pos := by
+  apply Fin.ext
+  simp [moveInputPos, pos.isLt]
+
+@[simp]
+lemma moveInputPos_leftBoundary {n : ℕ} :
+    moveInputPos (0 : Fin (n + 2)) (-1) = 0 := by
+  apply Fin.ext
+  simp [moveInputPos]
+
+@[simp]
+lemma moveInputPos_rightBoundary {n : ℕ} :
+    moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by
+  unfold moveInputPos
+  rw [dite_eq_right (by simp; omega)]
+
+/-- A left move away from the left input boundary decrements the native input position. -/
+lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) :
+    moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by
+  have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz))
+  unfold moveInputPos
+  apply Fin.ext
+  rw [dite_eq_left] <;> simp <;> omega
+
+/-- A right move away from the right input boundary increments the native input position. -/
+lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) :
+    moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by
+  unfold moveInputPos
+  rw [dite_eq_left]
+  · apply Fin.ext
+    simp
+  · simp
+    omega
+
+/-- The symbol currently under the input tape head. -/
+def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol :=
+  if h₁ : cfg.inputPos = 0 then none
+  else if h₂ : cfg.inputPos = input.length + 1 then none
+  else input[cfg.inputPos.val - 1]'(by grind)
+
+@[simp]
+lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ)
+    (h₁ : cfg.inputPos.val = 1 + p)
+    (h₂ : p < input.length) :
+    cfg.inputSymbol = some input[p] := by
+  grind [Cfg.inputSymbol]
+
+/-- The symbol read by work tape `i`. -/
+def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol :=
+  cfg.workTapes i (cfg.workTapePos i)
+
+/-- A configuration is halted when it has no state to continue from. -/
+abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none
+
+/-- The initial configuration for a starting state and an input string. -/
+@[simp]
+def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input :=
+  ⟨some q₀, 1, fun _ _ => none, fun _ => 0, []⟩
+
+/--
+The effect of an action on a configuration: move the input head, write and move on the work tapes,
+append the emitted symbol to the output tape, and go to the successor state. This is the part of a
+step that does not depend on how the action was chosen.
+-/
+@[simp]
+def Action.apply (out : Action k Symbol State) (cfg : Cfg k Symbol State input) :
+    Cfg k Symbol State input where
+  state := out.q'
+  inputPos := moveInputPos cfg.inputPos out.inputMove
+  workTapes i := match (out.workActions i).1 with
+    | none => cfg.workTapes i
+    | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s
+  workTapePos i := cfg.workTapePos i + (out.workActions i).2
+  output := cfg.output ++ out.outS.toList
+
+/-- A work tape head moves by at most one cell when an action is applied. -/
+lemma workTapePos_apply_le (out : Action k Symbol State)
+    (cfg : Cfg k Symbol State input) (i : Fin k) :
+    |(out.apply cfg).workTapePos i - cfg.workTapePos i| ≤ 1 := by
+  simp only [Action.apply, add_sub_cancel_left, abs_le, SignType.cast]
+  grind
+
+/-- The work tape cells visited by the head of tape `i` along a list of configurations. -/
+def visitedOfCfgs (cfgs : List (Cfg k Symbol State input)) (i : Fin k) : Finset ℤ :=
+  (cfgs.map (·.workTapePos i)).toFinset
+
+/-- The number of work tape cells touched by the heads along a list of configurations. -/
+def spaceUsedOfCfgs (cfgs : List (Cfg k Symbol State input)) : ℕ :=
+  ∑ i, (visitedOfCfgs cfgs i).card
+
+end Turing
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 625b932b2..ea4c0fd67 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
@@ -6,14 +6,10 @@ Authors: Christian Reitwiessner
 
 module
 
-public import Mathlib.Data.Finset.Max
-public import Mathlib.Data.Int.Interval
-public import Mathlib.Algebra.Order.Group.Abs
-public import Mathlib.Algebra.Order.Group.Int
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Computability.Language
-public import Mathlib.Data.Sign.Defs
 public import Cslib.Foundations.Data.RelatesInSteps
+public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
 
 /-!
 # Deterministic Multi-Tape Turing Machines
@@ -67,7 +63,6 @@ the sub-linear space modifications from chapter 2.5 with the following changes:
 We define a number of structures and concepts related to multi-tape Turing machine computation:
 
 * `MultiTapeTM`: the TM itself
-* `Cfg`: the configuration of a TM: the internal state, the work tape contents and head positions
 * `spaceUsed`: the number of work tape cells touched by the heads until a certain step
 * `TransitionRelation`: the transition relation from one configuration to the next
 * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure
@@ -81,7 +76,7 @@ We define a number of structures and concepts related to multi-tape Turing machi
 There are two ways to talk about the behaviour of a multi-tape Turing machine, and they are
 proven to be equivalent.
 
-* `MultiTapeTM.configs`: a sequence of configurations by execution step
+* `MultiTapeTM.runFrom`: the configuration reached after a given number of execution steps
 * `RelatesInSteps tm.TransitionRelation cfg cfg' t`: a proof that `tm` transforms the configuration
     `cfg` into `cfg'` in exactly `t` steps
 
@@ -101,20 +96,9 @@ namespace Turing
 
 variable {k : ℕ} {State Symbol : Type*}
 
-/-- The output of the transition function. -/
-structure TransitionOut (k : ℕ) (Symbol State : Type*) where
-  /-- The movement (attempt) of the input head. -/
-  inputMove : SignType
-  /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/
-  workActions : Fin k → (Option (Option Symbol)) × SignType
-  /-- An optional symbol to output. -/
-  outS : Option Symbol
-  /-- The successor state or none to halt. -/
-  q' : Option State
-
 /--
 A multi-tape Turing machine with `k` work tapes over the alphabet of `Option Symbol` (where `none`
-is the blank `BiTape` symbol). Note that it is not required that `Symbol` or `State` are finite
+is the blank tape symbol). Note that it is not required that `Symbol` or `State` are finite
 to keep the definition more general. The restriction will be introduced once we start talking about
 computability by Turing machines in general.
 -/
@@ -125,7 +109,7 @@ structure MultiTapeTM (k : ℕ) (Symbol State : Type*) where
   symbols to a movement for the input head, actions on the work tape, optionally a symbol to output
   and the successor state -/
   tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) :
-    TransitionOut k Symbol State
+    Action k Symbol State
 
 namespace MultiTapeTM
 
@@ -134,111 +118,19 @@ variable {tm : MultiTapeTM k Symbol State}
 section Cfg
 
 /-!
-## Configurations of a Turing Machine
-
-This section defines the configurations of a Turing machine,
-the step function that lets the machine transition from one configuration to the next,
-the resulting sequence of configurations and the initial configuration.
--/
+## Stepping a Turing Machine
 
-/--
-The configurations of a Turing machine is relative to the input of the machine and consist of:
-- an `Option`al state (or none for the halting state),
-- the position of the input head (shifted by one),
-- the contents of the work tape,
-- the positions of the work tape heads.
+This section defines the step function that lets the machine transition from one configuration to
+the next, and the configuration reached after a number of steps. Configurations themselves are
+defined in `Cslib.Computability.Machines.Turing.MultiTape.Configuration`.
 -/
-@[ext]
-structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where
-  /-- the state of the TM (or none for the halting state) -/
-  state : Option State
-  /-- the position of the input head, shifted by one -/
-  inputPos : Fin (input.length + 2)
-  /-- the work tapes -/
-  workTapes : Fin k → ℤ → Option Symbol
-  /-- the positions of the heads on the work tapes -/
-  workTapePos : Fin k → ℤ
-deriving Inhabited
-
-/-- Attempt to move the input tape head.
-The machine can only read one empty cell outside of the input,
-any attempted movement beyond that results in no movement.
-
-The addition is performed in `ℤ` before clamping. Performing it in `Fin (n + 2)` would wrap an
-outward boundary move to the opposite end of the input. -/
-@[scoped grind =]
-def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2) :=
-  let p := ((pos.val : ℤ) + (m.cast : ℤ)).toNat
-  if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩
-
-@[simp]
-lemma moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) :
-    moveInputPos pos 0 = pos := by
-  apply Fin.ext
-  simp [moveInputPos, pos.isLt]
-
-@[simp]
-lemma moveInputPos_leftBoundary {n : ℕ} :
-    moveInputPos (0 : Fin (n + 2)) (-1) = 0 := by
-  apply Fin.ext
-  simp [moveInputPos]
-
-@[simp]
-lemma moveInputPos_rightBoundary {n : ℕ} :
-    moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by
-  unfold moveInputPos
-  rw [dite_eq_right (by simp; omega)]
-
-/-- A left move away from the left input boundary decrements the native input position. -/
-lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) :
-    moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by
-  have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz))
-  unfold moveInputPos
-  apply Fin.ext
-  rw [dite_eq_left] <;> simp <;> omega
-
-/-- A right move away from the right input boundary increments the native input position. -/
-lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) :
-    moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by
-  unfold moveInputPos
-  rw [dite_eq_left]
-  · apply Fin.ext
-    simp
-  · simp
-    omega
-
-/-- The symbol currently under the input tape head. -/
-def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol :=
-  if h₁ : cfg.inputPos = 0 then none
-  else if h₂ : cfg.inputPos = input.length + 1 then none
-  else input[cfg.inputPos.val - 1]'(by grind)
-
-@[simp]
-lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ)
-    (h₁ : cfg.inputPos.val = 1 + p)
-    (h₂ : p < input.length) :
-    cfg.inputSymbol = some input[p] := by
-  grind [Cfg.inputSymbol]
-
-/-- The symbol read by work tape `i`. -/
-def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol :=
-  cfg.workTapes i (cfg.workTapePos i)
 
 /-- The step function corresponding to a `MultiTapeTM`. -/
 def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input :=
   match cfg.state with
   -- in the halting state, we stay at the configuration
   | none => cfg
-  | some q =>
-    let {inputMove, workActions, q', ..} := tm.tr q cfg.inputSymbol cfg.workTapeSymbols
-    {
-      state := q',
-      inputPos := moveInputPos cfg.inputPos inputMove,
-      workTapes i := match (workActions i).1 with
-        | none => cfg.workTapes i
-        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s
-      workTapePos i := (cfg.workTapePos i) + (workActions i).2
-    }
+  | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg
 
 /-- The symbol (optionally) output when executing one step starting from configuration `cfg`. -/
 def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol :=
@@ -248,8 +140,7 @@ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol :=
 
 /-- The initial configuration corresponding to an input string. -/
 @[simp]
-def initCfg (input : List Symbol) : Cfg k Symbol State input :=
-  ⟨some tm.q₀, 1, fun _ _ => none, fun _ => 0⟩
+def initCfg (input : List Symbol) : Cfg k Symbol State input := Cfg.init tm.q₀ input
 
 @[simp]
 lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) :
@@ -257,37 +148,37 @@ lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) :
   unfold step
   rw [h]
 
-/-- The sequence of configurations of the Turing machine starting from `cfg`.
+/-- The configuration reached by running the Turing machine for `t` steps from `cfg`.
 If the Turing machine halts, it will stay at the halting configuration. -/
-def configs (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg
+def runFrom (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg
 
 @[simp]
-lemma configs_zero {cfg : Cfg k Symbol State input} :
-    tm.configs cfg 0 = cfg := by
-  simp [configs]
-
-lemma configs_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} :
-    tm.configs cfg (t + 1) = tm.configs (tm.step cfg) t := by
-  simp [configs, Function.iterate_succ_apply]
-
-lemma configs_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} :
-    tm.configs cfg (t + 1) = tm.step (tm.configs cfg t) := by
-  simp [configs, Function.iterate_succ_apply']
-
-/-- Running `a + d` steps equals running `a` steps from the configuration reached after `d`. -/
-lemma configs_add (cfg : Cfg k Symbol State input) (a b : ℕ) :
-    tm.configs cfg (a + b) = tm.configs (tm.configs cfg a) b := by
-  unfold configs
+lemma runFrom_zero {cfg : Cfg k Symbol State input} :
+    tm.runFrom cfg 0 = cfg := by
+  simp [runFrom]
+
+lemma runFrom_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} :
+    tm.runFrom cfg (t + 1) = tm.runFrom (tm.step cfg) t := by
+  simp [runFrom, Function.iterate_succ_apply]
+
+lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} :
+    tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by
+  simp [runFrom, Function.iterate_succ_apply']
+
+/-- Running `a + b` steps equals running `b` steps from the configuration reached after `a`. -/
+lemma runFrom_add (cfg : Cfg k Symbol State input) (a b : ℕ) :
+    tm.runFrom cfg (a + b) = tm.runFrom (tm.runFrom cfg a) b := by
+  unfold runFrom
   rw [Nat.add_comm, Function.iterate_add_apply]
 
-/-- The sequence of configurations from a halting state is constant. -/
+/-- Running from a halting configuration stays at that configuration. -/
 @[simp]
-lemma configs_of_halts (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} :
-    tm.configs cfg n = cfg := by
+lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} :
+    tm.runFrom cfg n = cfg := by
   induction n with
   | zero => rfl
   | succ d ih =>
-    rw [configs_succ_eq_step', ih, step_of_halt h]
+    rw [runFrom_succ_eq_step', ih, step_of_halt h]
 
 @[simp]
 lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) :
@@ -300,9 +191,7 @@ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) :
   unfold step
   cases hstate : c.state with
   | none => simp
-  | some q =>
-    simp only [add_sub_cancel_left, abs_le, SignType.cast]
-    grind
+  | some q => exact workTapePos_apply_le _ c i
 
 end Cfg
 
@@ -312,7 +201,7 @@ section Space
 /-- The set of positions visited by the head of work tape `i` in the computation starting from
 configuration `cfg` up to step `t`. -/
 def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ :=
-  (Finset.range (t + 1)).image fun t' => (tm.configs cfg t').workTapePos i
+  (Finset.range (t + 1)).image fun t' => (tm.runFrom cfg t').workTapePos i
 
 /--
 The number of work tape cells touched by the head of tape `i` in the computation starting from
@@ -340,6 +229,14 @@ lemma spaceUsedByTape_le_spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) (i
     tm.spaceUsedByTape cfg t i ≤ tm.spaceUsed cfg t :=
   Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)
 
+/-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/
+lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) :
+    tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := by
+  unfold spaceUsed spaceUsedByTape spaceUsedOfCfgs
+  refine Finset.sum_congr rfl fun i _ => congrArg Finset.card ?_
+  ext z
+  simp [visitedByTapeHead, visitedOfCfgs, Nat.lt_succ_iff]
+
 end Space
 
 open Cfg
@@ -352,54 +249,21 @@ which maps a configuration to its next configuration.
 @[scoped grind =]
 def TransitionRelation (c₁ c₂ : Cfg k Symbol State input) : Prop := tm.step c₁ = c₂
 
-/-- The string output by the Turing machine `tm` starting in configuration `cfg₀`, executing for
-`t` steps. It is the concatenation of the symbols (optionally) emitted at each of the first `t`
-steps. -/
-def outputString
-    (tm : MultiTapeTM k Symbol State)
-    (cfg₀ : Cfg k Symbol State input) (t : ℕ) : List Symbol :=
-  (List.range t).flatMap fun t' => (tm.outputSymbol (tm.configs cfg₀ t')).toList
-
-/-- The output produced in `t + 1` steps is the output produced in `t` steps followed by the symbol
-(optionally) emitted at step `t`. -/
-lemma outputString_succ
-    (tm : MultiTapeTM k Symbol State)
-    (cfg : Cfg k Symbol State input) (t : ℕ) :
-    tm.outputString cfg (t + 1) =
-      tm.outputString cfg t ++ (tm.outputSymbol (tm.configs cfg t)).toList := by
-  simp [outputString, List.range_succ, List.flatMap_append]
-
-/-- From a halting configuration, a TM does not output anything. -/
-lemma outputString_halt
-    (tm : MultiTapeTM k Symbol State)
-    (cfg : Cfg k Symbol State input)
-    (h_halt : cfg.state = none)
-    (t : ℕ) :
-    tm.outputString cfg t = [] := by
-  induction t with
-  | zero => simp [outputString]
-  | succ t ih => simp [outputString_succ, ih, h_halt]
-
-lemma outputString_add_eq_append
-    (tm : MultiTapeTM k Symbol State)
-    (cfg : Cfg k Symbol State input) (t₁ t₂ : ℕ) :
-    tm.outputString cfg (t₁ + t₂) =
-      tm.outputString cfg t₁ ++ tm.outputString (tm.configs cfg t₁) t₂ := by
-  induction t₂ with
-  | zero => simp [outputString]
-  | succ t ih =>
-    rw [show (t₁ + (t + 1)) = (t₁ + t) + 1 by omega]
-    simp [outputString_succ, ih, configs, ← Function.iterate_add_apply, Nat.add_comm]
+/-- One step appends the symbol (optionally) emitted by that step to the output tape. -/
+@[simp]
+lemma step_output (cfg : Cfg k Symbol State input) :
+    (tm.step cfg).output = cfg.output ++ (tm.outputSymbol cfg).toList := by
+  unfold step outputSymbol Action.apply
+  cases cfg.state <;> simp
 
 /-- The output does not change after the machine has halted. -/
-lemma outputString_eq_of_halt
+lemma runFrom_output_eq_of_halt
     (tm : MultiTapeTM k Symbol State)
     (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)
-    (hhalt : (tm.configs cfg τ).state = none) :
-    tm.outputString cfg t = tm.outputString cfg τ := by
+    (hhalt : (tm.runFrom cfg τ).state = none) :
+    (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output := by
   conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm]
-  rw [outputString_add_eq_append, outputString_halt _ _ hhalt]
-  simp
+  rw [runFrom_add, runFrom_of_halt _ hhalt]
 
 /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps
 and uses exactly `s` space.
@@ -408,8 +272,8 @@ def ComputesInTimeAndSpace
     (tm : MultiTapeTM k Symbol State)
     (input output : List Symbol)
     (t s : ℕ) : Prop :=
-  (tm.configs (tm.initCfg input) t).state = none ∧
-  tm.outputString (tm.initCfg input) t = output ∧
+  (tm.runFrom (tm.initCfg input) t).state = none ∧
+  (tm.runFrom (tm.initCfg input) t).output = output ∧
   tm.spaceUsed (tm.initCfg input) t = s
 
 /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of
@@ -453,19 +317,19 @@ def DecidableInTimeAndSpace
 /-- This lemma translates between the relational notion and the iterated step notion. The latter
 can be more convenient especially for deterministic machines as we have here. -/
 @[scoped grind =]
-lemma relatesInSteps_iff_configs_eq
+lemma relatesInSteps_iff_runFrom_eq
     (tm : MultiTapeTM k Symbol State)
     (cfg₁ cfg₂ : Cfg k Symbol State input)
     (t : ℕ) :
-    RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔ tm.configs cfg₁ t = cfg₂ := by
-  unfold configs
+    RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by
+  unfold runFrom
   induction t generalizing cfg₁ cfg₂ with
   | zero => simp
   | succ t ih =>
     rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply']
     constructor
     · grind
-    · intro h_configs
+    · intro h_runFrom
       use tm.step^[t] cfg₁
       grind
 
@@ -473,8 +337,8 @@ lemma relatesInSteps_iff_configs_eq
 if its state is `none` at step `t` and non-none at step `t - 1`.
 Note that every Turing machine hast to perform at least one step to halt. -/
 def haltsAtStep (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : Bool :=
-  (tm.configs (tm.initCfg input) t).state.isNone &&
-  !(tm.configs (tm.initCfg input) (t - 1)).state.isNone
+  (tm.runFrom (tm.initCfg input) t).state.isNone &&
+  !(tm.runFrom (tm.initCfg input) (t - 1)).state.isNone
 
 /-- If a Turing machine halts, the time step is uniquely determined. -/
 lemma halting_step_unique
@@ -490,39 +354,39 @@ lemma halting_step_unique
   cases d with
   | zero => rfl
   | succ d =>
-    have halts₁ : (tm.configs (tm.initCfg input) t₁).state = none := by
+    have halts₁ : (tm.runFrom (tm.initCfg input) t₁).state = none := by
       simp [haltsAtStep] at h_halts₁
       exact h_halts₁.left
-    have halts₂ : (tm.configs (tm.initCfg input) (d + t₁)).state ≠ none := by
-      grind [haltsAtStep, configs]
+    have halts₂ : (tm.runFrom (tm.initCfg input) (d + t₁)).state ≠ none := by
+      grind [haltsAtStep, runFrom]
     refine absurd ?_ halts₂
-    rw [Nat.add_comm, configs_add, tm.configs_of_halts _ halts₁]
+    rw [Nat.add_comm, runFrom_add, tm.runFrom_of_halt _ halts₁]
     exact halts₁
 
 /-- If a deterministic machine repeats a non-halting configuration, it never halts,
 because the sequence between the two configurations will loop forever.
 Note that this can be applied to two arbitrary and different time steps `t` and `t + Δ`
-using `tm.configs_add`. -/
+using `tm.runFrom_add`. -/
 lemma not_halts_of_repeat_nonhalt
     (cfg : Cfg k Symbol State input)
     (h_not_halt : cfg.state ≠ none)
     (t : ℕ)
-    (heq : tm.configs cfg (t + 1) = cfg) :
-    ∀ t', (tm.configs cfg t').state ≠ none := by
+    (heq : tm.runFrom cfg (t + 1) = cfg) :
+    ∀ t', (tm.runFrom cfg t').state ≠ none := by
   intro t'
   -- The configuration will repeat every `t + 1` steps.
-  have hloop : ∀ n, tm.configs cfg (n * (t + 1)) = cfg := by
+  have hloop : ∀ n, tm.runFrom cfg (n * (t + 1)) = cfg := by
     intro n
     induction n with
     | zero => simp
     | succ n ih =>
-      rw [show (n + 1) * (t + 1) = n * (t + 1) + (t + 1) by grind, tm.configs_add, ih, heq]
+      rw [show (n + 1) * (t + 1) = n * (t + 1) + (t + 1) by grind, tm.runFrom_add, ih, heq]
   by_contra hnh
   -- Assuming the machine halts at step `t'`, it is also halted at step `t' * (t + 1)`
-  have h₁ : (tm.configs cfg (t' * (t + 1))).state = none := by
+  have h₁ : (tm.runFrom cfg (t' * (t + 1))).state = none := by
     have hle : t' ≤ t' * (t + 1) := by grind
     obtain ⟨tΔ , htΔ⟩ := Nat.exists_eq_add_of_le hle
-    rw [htΔ, tm.configs_add]
+    rw [htΔ, tm.runFrom_add]
     simp [hnh]
   simp [hloop t', h_not_halt] at h₁
 
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean
new file mode 100644
index 000000000..091a3615f
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean
@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
+
+/-!
+# Deterministic Multi-Tape Turing Machines are Nondeterministic
+
+Embeds `MultiTapeTM` into `MultiTapeNTM` and shows the embedding preserves computation.
+
+`toNTM` permits exactly the transition `tr` prescribes: nondeterminism is the possibility of
+several, so having exactly one is the special case. A deterministic computation is then witnessed
+by the machine's own run. Both models idle once the machine has halted, so that run has exactly
+`t` steps for every `t` and its measures match `runFrom` and `spaceUsed` directly, with no
+reasoning about the step at which the machine halted.
+
+## Important Declarations
+
+* `MultiTapeTM.toNTM`: every deterministic machine is a nondeterministic one
+* `MultiTapeTM.toNTMComputationPath`: the machine's own run, as a computation of `toNTM`
+* `MultiTapeTM.toNTM_computes`: every deterministic computation is a nondeterministic one
+-/
+
+@[expose] public section
+
+namespace Turing
+
+variable {k : ℕ} {State Symbol : Type*} {input : List Symbol}
+
+/-- Every deterministic machine is a nondeterministic one whose relation is a singleton. -/
+def MultiTapeTM.toNTM (tm : MultiTapeTM k Symbol State) : MultiTapeNTM k Symbol State where
+  q₀ := tm.q₀
+  Tr q input work out := out = tm.tr q input work
+
+namespace MultiTapeTM
+
+variable {tm : MultiTapeTM k Symbol State} {t : ℕ}
+
+@[simp]
+lemma toNTM_initCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) :
+    tm.toNTM.initCfg input = tm.initCfg input := rfl
+
+/-- Each step of `tm` is a step of its nondeterministic reading. This holds at a halted
+configuration too, where both models idle. -/
+theorem toNTM_step (c : Cfg k Symbol State input) : tm.toNTM.Step c (tm.step c) := by
+  cases hq : c.state <;> simp [MultiTapeNTM.Step, step, toNTM, hq]
+
+/-- The machine's own run for `t` steps, as a computation of its nondeterministic reading: the
+configuration reached after each step. -/
+def toNTMComputationPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) :
+    tm.toNTM.ComputationPath input where
+  length := t
+  toFun i := tm.runFrom (tm.initCfg input) i
+  step i := by
+    simp only [Fin.val_castSucc, Fin.val_succ, runFrom_succ_eq_step']
+    exact toNTM_step _
+  head_eq := rfl
+
+@[simp]
+lemma toNTMComputationPath_length : (tm.toNTMComputationPath input t).length = t := rfl
+
+@[simp]
+lemma toNTMComputationPath_last :
+    (tm.toNTMComputationPath input t).last = tm.runFrom (tm.initCfg input) t := rfl
+
+@[simp]
+lemma toNTMComputationPath_toList :
+    (tm.toNTMComputationPath input t).toList
+      = (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) := by
+  rw [RelSeries.toList, ← List.map_coe_finRange_eq_range, List.map_map]
+  exact List.ofFn_eq_map
+
+@[simp]
+lemma toNTMComputationPath_space :
+    (tm.toNTMComputationPath input t).space = tm.spaceUsed (tm.initCfg input) t := by
+  simp [MultiTapeNTM.ComputationPath.space, spaceUsed_eq_spaceUsedOfCfgs]
+
+/-- Every deterministic computation is a nondeterministic one, witnessed by the machine's own
+run. -/
+theorem toNTM_computes {output : List Symbol} {t s : ℕ}
+    (h : tm.ComputesInTimeAndSpace input output t s) :
+    tm.toNTM.ComputesInTimeAndSpace input output t s :=
+  ⟨tm.toNTMComputationPath input t, h.1, h.2.1, toNTMComputationPath_length,
+    toNTMComputationPath_space.trans h.2.2⟩
+
+end MultiTapeTM
+
+end Turing
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
new file mode 100644
index 000000000..64f72a50c
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+module
+
+public import Mathlib.Data.List.Chain
+public import Mathlib.Order.RelSeries
+public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
+
+/-!
+# Nondeterministic Multi-Tape Turing Machines
+
+Defines nondeterministic Turing machines with a read-only input tape, `k` work tapes and one
+write-only output tape, and what it means for one to compute an output within a time and space
+bound.
+
+## Design
+
+Following [Papadimitriou94], chapter 2.7, a nondeterministic machine is a Turing machine whose
+transition function is replaced by a transition relation: `Tr q input work action` holds when
+`action` is one of the actions permitted in that situation.
+
+A halted configuration steps to itself, so once a machine has halted it has a run of every length.
+A time bound is therefore an upper bound, with no separate account of the step at which it halted.
+
+The transition relation may be empty at a running configuration, so a machine can get stuck. Every
+notion below asks for a computation ending in a halted configuration, so a stuck one is not a
+witness.
+
+## Important Declarations
+
+* `MultiTapeNTM`: the machine, an initial state and a transition relation
+* `Step`: the one-step relation on configurations
+* `ComputationPath`: a run of the machine: a series of configurations from the initial one, each
+    reached from the previous by a step
+* `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint
+* `Computes`, `ComputesInTime`, `ComputesInSpace`, `ComputesInTimeAndSpace`: its instances, whose
+    bounds all refer to a single computation
+
+## References
+
+* [C. Papadimitriou, *Computational Complexity*][Papadimitriou94]
+* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013]
+-/
+
+@[expose] public section
+
+namespace Turing
+
+variable {k : ℕ} {State Symbol : Type*} {input : List Symbol}
+
+/--
+A nondeterministic multi-tape Turing machine with `k` work tapes over the alphabet of
+`Option Symbol` (where `none` is the blank symbol). Neither `Symbol` nor `State` is required to be
+finite.
+-/
+structure MultiTapeNTM (k : ℕ) (Symbol State : Type*) where
+  /-- initial state -/
+  q₀ : State
+  /-- transition relation: which combinations of state, current input symbol, tuple of work head
+  symbols and resulting actions are valid transitions -/
+  Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol)
+    (action : Action k Symbol State) : Prop
+
+namespace MultiTapeNTM
+
+variable {ntm : MultiTapeNTM k Symbol State}
+
+/-- The one-step relation on configurations. A halted configuration steps to itself; a running one
+steps by any permitted transition. -/
+@[scoped grind =]
+def Step (ntm : MultiTapeNTM k Symbol State) (c₁ c₂ : Cfg k Symbol State input) : Prop :=
+  match c₁.state with
+  | none => c₂ = c₁
+  | some q => ∃ out, ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols out ∧ c₂ = out.apply c₁
+
+/-- A halted configuration steps only to itself. -/
+lemma step_of_halt {c c' : Cfg k Symbol State input} (h : c.Halted) :
+    ntm.Step c c' ↔ c' = c := by
+  simp [Step, h]
+
+/-- The initial configuration corresponding to an input string. -/
+@[simp]
+def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) :
+    Cfg k Symbol State input :=
+  Cfg.init ntm.q₀ input
+
+/-- A computation path of `ntm` on `input`: a series of configurations starting at the initial one,
+in which each is reached from the previous by a step. `RelSeries` supplies the series itself, so
+`length` is the number of steps taken, `toList` the configurations passed through, and `last` the
+one it ends at.
+Note that it is not required that the machine terminates at the final configuration of the path. -/
+structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol)
+    extends RelSeries {(c₁, c₂) : Cfg k Symbol State input × _ | ntm.Step c₁ c₂} where
+  /-- a computation starts at the initial configuration -/
+  head_eq : toRelSeries.head = ntm.initCfg input
+
+namespace ComputationPath
+
+variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol}
+
+/-- The number of work tape cells touched. -/
+def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.toList
+
+end ComputationPath
+
+/-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits
+`output` and satisfies `P`. The notions below are its instances, so their constraints all refer to
+a single computation. -/
+def ComputesSuchThat (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol)
+    (P : ntm.ComputationPath input → Prop) : Prop :=
+  ∃ p : ntm.ComputationPath input, p.last.Halted ∧ p.last.output = output ∧ P p
+
+/-- `ntm` computes `output` from `input`, with no bound on resources. -/
+def Computes (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) : Prop :=
+  ntm.ComputesSuchThat input output fun _ => True
+
+/-- `ntm` computes `output` from `input` in exactly `t` steps. -/
+def ComputesInTime (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t : ℕ) :
+    Prop :=
+  ntm.ComputesSuchThat input output fun p => p.length = t
+
+/-- `ntm` computes `output` from `input` touching exactly `s` work tape cells. -/
+def ComputesInSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (s : ℕ) :
+    Prop :=
+  ntm.ComputesSuchThat input output fun p => p.space = s
+
+/-- `ntm` computes `output` from `input` in `t` steps and `s` work tape cells, by a single
+computation. Nondeterministic analogue of `MultiTapeTM.ComputesInTimeAndSpace`. -/
+def ComputesInTimeAndSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol)
+    (t s : ℕ) : Prop :=
+  ntm.ComputesSuchThat input output fun p => p.length = t ∧ p.space = s
+
+end MultiTapeNTM
+
+end Turing
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
index 39ec30f56..15145637a 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
@@ -42,11 +42,11 @@ lemma step_workTapes_eq_of_ne
     rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> simp_all
 
 lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} :
-    z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.configs cfg t').workTapePos i = z := by
+    z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by
   simp [visitedByTapeHead]
 
 lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    (tm.configs cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i :=
+    (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. -/
@@ -59,14 +59,14 @@ lemma visitedByTapeHead_mono (cfg : Cfg k Symbol State input) (i : Fin k) {t t'
 `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.configs cfg t).workTapePos i)
+    Finset.uIcc (cfg.workTapePos i) ((tm.runFrom cfg t).workTapePos i)
       ⊆ tm.visitedByTapeHead cfg t i := by
   induction t with
-  | zero => simpa [configs] using tm.mem_visitedByTapeHead_self cfg 0 i
+  | zero => simpa [runFrom] using tm.mem_visitedByTapeHead_self cfg 0 i
   | succ t ih =>
     intro z hz
-    have hstep : |(tm.configs cfg (t + 1)).workTapePos i - (tm.configs cfg t).workTapePos i| ≤ 1 :=
-      configs_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ i
+    have hstep : |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 :=
+      runFrom_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ 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]
@@ -76,13 +76,13 @@ lemma mem_visitedByTapeHead_of_workTapes_ne
     (j : Fin k)
     (t : ℕ)
     (z : ℤ)
-    (h : (tm.configs cfg t).workTapes j z ≠ cfg.workTapes j 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 [configs]) h
+  | zero => exact absurd (by simp [runFrom]) h
   | succ t ih =>
-    rw [configs_succ_eq_step'] at h
-    by_cases hz : z = (tm.configs cfg t).workTapePos j
+    rw [runFrom_succ_eq_step'] 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
@@ -109,7 +109,7 @@ lemma content_natAbs_le_spaceUsedByTape
     {i : Fin k}
     (t : ℕ)
     (z : ℤ)
-    (h : (tm.configs (tm.initCfg input) t).workTapes i z ≠ none) :
+    (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.