diff --git a/Cslib.lean b/Cslib.lean
index 1d0469a56..9b3595870 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -46,7 +46,9 @@ 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.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..45cde39f1
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean
@@ -0,0 +1,236 @@
+/-
+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, moving a head by at most one
+    cell (`workTapePos_apply_le`) and changing no cell but the one under it
+    (`workTapes_apply_eq_of_ne`)
+* `Cfg.stepWith`, `Cfg.StepWith`: one step, choosing an action by a function or by a relation,
+    agreeing via `Cfg.stepWith_iff` when the relation is the function's graph
+* `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in
+* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations, with the bounds
+    `spaceUsedOfCfgs_le` and `spaceUsedOfCfgs_mono`
+-/
+
+@[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
+
+/-- One step from `cfg`, choosing an action with `f`. A halted configuration idles. -/
+@[simp]
+def Cfg.stepWith (cfg : Cfg k Symbol State input) (f : State → Action k Symbol State) :
+    Cfg k Symbol State input :=
+  match cfg.state with
+  | none => cfg
+  | some q => (f q).apply cfg
+
+/-- One step from `cfg`, choosing any action permitted by `R`. A halted configuration idles. -/
+def Cfg.StepWith (cfg cfg' : Cfg k Symbol State input)
+    (R : State → Action k Symbol State → Prop) : Prop :=
+  match cfg.state with
+  | none => cfg' = cfg
+  | some q => ∃ a, R q a ∧ cfg' = a.apply cfg
+
+/-- Choosing from the graph of a function is choosing that function's value: there is exactly one
+step. This is what makes a machine deterministic, said without mentioning one. -/
+theorem Cfg.stepWith_iff {cfg cfg' : Cfg k Symbol State input} {f : State → Action k Symbol State}
+    {R : State → Action k Symbol State → Prop} (h : ∀ q a, R q a ↔ a = f q) :
+    cfg.StepWith cfg' R ↔ cfg' = cfg.stepWith f := by
+  cases hq : cfg.state <;> simp [Cfg.StepWith, Cfg.stepWith, hq, h]
+
+/-- 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
+
+/-- An action only changes the cell its head is on, so a cell elsewhere is left alone. -/
+lemma workTapes_apply_eq_of_ne (a : Action k Symbol State) (cfg : Cfg k Symbol State input)
+    (j : Fin k) (z : ℤ) (hz : z ≠ cfg.workTapePos j) :
+    (a.apply cfg).workTapes j z = cfg.workTapes j z := by
+  rcases hw : (a.workActions j).1 <;> simp_all
+
+/-- 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
+
+/-- Each configuration contributes at most one cell per tape, so space is bounded by length. -/
+theorem spaceUsedOfCfgs_le (cfgs : List (Cfg k Symbol State input)) :
+    spaceUsedOfCfgs cfgs ≤ k * cfgs.length := by
+  calc spaceUsedOfCfgs cfgs
+      ≤ ∑ _i : Fin k, cfgs.length :=
+        Finset.sum_le_sum fun i _ => (List.toFinset_card_le _).trans (by simp)
+    _ = k * cfgs.length := by simp
+
+/-- Passing through more configurations touches more cells. -/
+theorem spaceUsedOfCfgs_mono {c d : List (Cfg k Symbol State input)} (h : c.Sublist d) :
+    spaceUsedOfCfgs c ≤ spaceUsedOfCfgs d :=
+  Finset.sum_le_sum fun i _ => Finset.card_le_card <| by
+    intro z hz
+    simp only [visitedOfCfgs, List.mem_toFinset] at hz ⊢
+    exact (h.map _).subset hz
+
+end Turing
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 3d460e45a..beaeaddee 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.Nondeterministic
 
 /-!
 # Deterministic Multi-Tape Turing Machines
@@ -62,18 +58,24 @@ the sub-linear space modifications from chapter 2.5 with the following changes:
   and not by a restriction on the transition function. The two definitions are equivalent, but
   not restricting the transition function makes it easier to define a universal machine.
 
+`MultiTapeTM` extends `MultiTapeNTM` with a transition function and the requirement that the
+permitted transitions are exactly the ones it prescribes. `Step`, `ComputationPath` and the
+`Computes` notions of the nondeterministic machine therefore apply unchanged, and what this file
+adds is what follows from there being no choice to make.
+
 ## Important Declarations
 
 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,
-    and the output tape
-* `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
-* `ComputesInTimeAndSpace`: a proof that a specific TM computes an output from an input in a certain
-    number of steps and using a certain number of tape cells
+* `MultiTapeTM`: the TM itself, a `MultiTapeNTM` whose transition relation is a function
+* `ofTr`: the machine with a given initial state and transition function
+* `runPath`: the machine's own run from a configuration, as a `ComputationPath`
+* `runFrom`: the configuration that run ends in, equal to iterating `step` (`runFrom_eq_iterate`)
+* `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure;
+    the space of that run
+* `step_iff`: the inherited `Step` is the graph of `step`
+* `computesInExactTimeAndSpace_iff_runFrom`: the inherited `ComputesInExactTimeAndSpace`, stated
+    by step index rather than by computation path, via `ComputationPath.cfgs_eq`
 * `ComputableInTimeAndSpace`: a proof that there is a multi-tape TM that computes a function
     (on strings) respecting a time and space bound in the input length.
 * `DecidableInTimeAndSpace`: a proof that a TM decides a language within a certain time
@@ -83,7 +85,7 @@ There are two ways to talk about the behaviour of a multi-tape Turing machine, a
 proven to be equivalent.
 
 * `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
+* `RelatesInSteps tm.Step cfg cfg' t`: a proof that `tm` transforms the configuration
     `cfg` into `cfg'` in exactly `t` steps
 
 ## References
@@ -102,31 +104,33 @@ 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 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.
 -/
-structure MultiTapeTM (k : ℕ) (Symbol State : Type*) where
-  /-- initial state -/
-  q₀ : State
+structure MultiTapeTM (k : ℕ) (Symbol State : Type*)
+    extends MultiTapeNTM k Symbol State where
   /-- transition function, mapping a state, the current input symbol and a tuple of work head
   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
+  /-- the permitted transitions are exactly the one `tr` prescribes -/
+  Tr_iff (q : State) (i : Option Symbol) (w : Fin k → Option Symbol)
+    (action : Action k Symbol State) : Tr q i w action ↔ action = tr q i w
+
+attribute [simp] MultiTapeTM.Tr_iff
+
+/-- The deterministic machine with initial state `q₀` and transition function `tr`. -/
+def MultiTapeTM.ofTr (q₀ : State)
+    (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) :
+    MultiTapeTM k Symbol State where
+  q₀ := q₀
+  Tr q i w action := action = tr q i w
+  tr := tr
+  Tr_iff _ _ _ _ := Iff.rfl
 
 namespace MultiTapeTM
 
@@ -135,157 +139,70 @@ variable {tm : MultiTapeTM k Symbol State}
 section Cfg
 
 /-!
-## Configurations of a Turing Machine
+## Stepping 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.
+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`.
 -/
 
-/--
-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)
-
 /-- 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', outS, ..} := 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
-      output := cfg.output ++ outS.toList
-    }
-
-/-- The symbol (optionally) output when executing one step starting from configuration `cfg`. -/
-def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol :=
-  match cfg.state with
-  | none => none
-  | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).outS
-
-/-- The initial configuration corresponding to an input string. -/
+  cfg.stepWith fun q => tm.tr q cfg.inputSymbol cfg.workTapeSymbols
+
+/-- `Step` is the relation `step` induces: from each configuration there is exactly one step.
+Everything below about a deterministic machine rests on this. -/
 @[simp]
-def initCfg (input : List Symbol) : Cfg k Symbol State input :=
-  ⟨some tm.q₀, 1, fun _ _ => none, fun _ => 0, []⟩
+theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c :=
+  Cfg.stepWith_iff (by simp)
 
+/-- A halted configuration steps to itself, inherited from `MultiTapeNTM`. -/
 @[simp]
 lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) :
-    tm.step cfg = cfg := by
-  unfold step
-  rw [h]
+    tm.step cfg = cfg :=
+  (MultiTapeNTM.step_of_halt h).mp (step_iff.mpr rfl)
 
-/-- 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 runFrom (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg
+/-- The machine's own run from `cfg` for `t` steps: it does nothing, or takes one more step. -/
+def runPath (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) :
+    ℕ → tm.ComputationPath input
+  | 0 => .single cfg
+  | t + 1 => (tm.runPath cfg t).concat (tm.step (tm.runPath cfg t).last) (step_iff.mpr rfl)
+
+/-- The configuration reached by running the Turing machine for `t` steps from `cfg`: the one its
+run ends in. If the Turing machine halts, it will stay at the halting configuration. -/
+def runFrom (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) :
+    Cfg k Symbol State input := (tm.runPath cfg t).last
 
 @[simp]
-lemma runFrom_zero {cfg : Cfg k Symbol State input} :
-    tm.runFrom cfg 0 = cfg := by
-  simp [runFrom]
+lemma runPath_last (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.runPath cfg t).last = tm.runFrom cfg t := rfl
 
-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]
+@[simp]
+lemma runFrom_zero {cfg : Cfg k Symbol State input} : tm.runFrom cfg 0 = cfg := rfl
 
 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']
+  simp only [runFrom, runPath, MultiTapeNTM.ComputationPath.concat_last]
+
+/-- The run ends where iterating `step` lands. Building the run says what running *is*; iterating
+says how to *do* it, and carries the `Function.iterate` API. -/
+theorem runFrom_eq_iterate (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input)
+    (t : ℕ) : tm.runFrom cfg t = tm.step^[t] cfg := by
+  induction t with
+  | zero => simp
+  | succ n ih =>
+    rw [runFrom_succ_eq_step', ih]
+    exact (Function.iterate_succ_apply' _ _ _).symm
+
+/-- How `runFrom` is evaluated: iterating `step`, rather than building the run it ends. -/
+def runFromIter (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) :
+    Cfg k Symbol State input := tm.step^[t] cfg
 
-/-- 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]
+@[csimp]
+theorem runFrom_eq_runFromIter : @runFrom = @runFromIter := by
+  funext k State Symbol input tm cfg t
+  exact tm.runFrom_eq_iterate cfg t
 
-/-- Running from a halting configuration stays at that configuration. -/
 @[simp]
 lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} :
     tm.runFrom cfg n = cfg := by
@@ -294,30 +211,51 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n
   | succ d ih =>
     rw [runFrom_succ_eq_step', ih, step_of_halt h]
 
+end Cfg
+
+
+open Cfg
+
+
+/-! ## Determinism
+
+`MultiTapeTM` extends `MultiTapeNTM`, so `Step`, `ComputationPath` and the `Computes` notions
+already apply to it; only the facts below are specific to having a transition function. They say
+that there is no choice to make: `Step` is the graph of `step`, so a computation path can only
+follow `runFrom`, and `runPath` shows there is one of every length.
+-/
+
+/-- Its run takes `t` steps. -/
 @[simp]
-lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) :
-    tm.outputSymbol cfg = none := by
-  simp [outputSymbol, h_halt]
-
-/-- 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
-  unfold step
-  cases hstate : c.state with
-  | none => simp
-  | some q =>
-    simp only [add_sub_cancel_left, abs_le, SignType.cast]
-    grind
+lemma runPath_time (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).time = t := by
+  induction t with
+  | zero => rfl
+  | succ n ih => simp [runPath, ih]
 
-end Cfg
+/-- Its run starts where it was asked to. -/
+@[simp]
+lemma runPath_start (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.runPath cfg t).start = cfg := by
+  induction t with
+  | zero => rfl
+  | succ n ih => simp [runPath, ih]
+
+/-- Its run passes through the configurations reached after each step. -/
+lemma runPath_cfgs (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.runPath cfg t).cfgs = (List.range (t + 1)).map (tm.runFrom cfg) := by
+  induction t with
+  | zero => rfl
+  | succ n ih =>
+    rw [runPath, MultiTapeNTM.ComputationPath.concat_cfgs, ih]
+    simp [List.range_succ, runFrom_succ_eq_step']
 
 section Space
-/-! Now we define space usage and add some helper lemmas. -/
+/-! Space is read off the machine's own run, so it is the space of a `ComputationPath`. -/
 
 /-- 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.runFrom cfg t').workTapePos i
+  visitedOfCfgs (tm.runPath cfg t).cfgs i
 
 /--
 The number of work tape cells touched by the head of tape `i` in the computation starting from
@@ -328,61 +266,45 @@ def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ
 
 /--
 The number of work tape cells touched by a computation starting from configuration
-`cfg` up to step `t`.
+`cfg` up to step `t`: the space of the machine's own run.
 -/
-def spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := ∑ i, tm.spaceUsedByTape cfg t i
+def spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := (tm.runPath cfg t).space
 
-/-- A zero-tape Turing machine uses zero space. -/
+/-- The space used up to step `t` is the space of the run up to step `t`. -/
 @[simp]
-lemma spaceUsed_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) :
-    tm.spaceUsed cfg t = 0 := by
-  unfold spaceUsed
-  subst h_zero
-  simp
+lemma runPath_space (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.runPath cfg t).space = tm.spaceUsed cfg t := rfl
 
-/-- Each tape's space usage is bounded by the total space used. -/
-lemma spaceUsedByTape_le_spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    tm.spaceUsedByTape cfg t i ≤ tm.spaceUsed cfg t :=
-  Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)
+/-- Space is the sum over the tapes of the cells each head touched. -/
+lemma spaceUsed_eq_sum (cfg : Cfg k Symbol State input) (t : ℕ) :
+    tm.spaceUsed cfg t = ∑ i, tm.spaceUsedByTape cfg t i := rfl
 
-end Space
+/-- 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
+  rw [spaceUsed, MultiTapeNTM.ComputationPath.space, runPath_cfgs]
 
-open Cfg
-
-/--
-The `TransitionRelation` corresponding to a `MultiTapeTM k Symbol`
-is defined by the `step` function,
-which maps a configuration to its next configuration.
--/
-@[scoped grind =]
-def TransitionRelation (c₁ c₂ : Cfg k Symbol State input) : Prop := tm.step c₁ = c₂
-
-/-- 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
-  cases cfg.state <;> simp
+end Space
 
-/-- The output does not change after the machine has halted. -/
-lemma runFrom_output_eq_of_halt
-    (tm : MultiTapeTM k Symbol State)
-    (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)
-    (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 [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.
-Note that this does not require the alphabet or state set to be finite. -/
-def ComputesInTimeAndSpace
-    (tm : MultiTapeTM k Symbol State)
-    (input output : List Symbol)
-    (t s : ℕ) : Prop :=
-  (tm.runFrom (tm.initCfg input) t).state = none ∧
-  (tm.runFrom (tm.initCfg input) t).output = output ∧
-  tm.spaceUsed (tm.initCfg input) t = s
+/-- `tm` has exactly one computation path of each length, so `ComputesInExactTimeAndSpace`,
+inherited from `MultiTapeNTM`, is the direct statement about `runFrom` and `spaceUsed` at step
+`t`. -/
+theorem computesInExactTimeAndSpace_iff_runFrom {input output : List Symbol} {t s : ℕ} :
+    tm.ComputesInExactTimeAndSpace input output t s ↔
+      (tm.runFrom (tm.initCfg input) t).state = none ∧
+      (tm.runFrom (tm.initCfg input) t).output = output ∧
+      tm.spaceUsed (tm.initCfg input) t = s := by
+  constructor
+  · rintro ⟨p, hstart, hhalt, hout, rfl, hspace⟩
+    have hp : p = tm.runPath (tm.initCfg input) p.time :=
+      MultiTapeNTM.ComputationPath.eq_of_start_of_time
+        (fun h₁ h₂ => (step_iff.mp h₁).trans (step_iff.mp h₂).symm)
+        (by simpa using hstart) (by simp)
+    rw [hp] at hhalt hout hspace
+    exact ⟨by simpa using hhalt, by simpa using hout, by simpa using hspace⟩
+  · rintro ⟨hhalt, hout, hspace⟩
+    exact ⟨tm.runPath (tm.initCfg input) t, by simp, by simpa using hhalt, by simpa using hout,
+      by simp, by simpa using hspace⟩
 
 /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of
 length `n` it uses at most `t n` steps and `s n` space. It assumes an embedding function
@@ -395,7 +317,7 @@ def ComputesFunInTimeAndSpace
     (toMachineSymbol : IOSymbol ↪ Symbol)
     (t s : ℕ → ℕ) : Prop :=
   ∀ input, ∃ t' ≤ t input.length, ∃ s' ≤ s input.length,
-  ComputesInTimeAndSpace tm (input.map toMachineSymbol) ((f input).map toMachineSymbol) t' s'
+  tm.ComputesInExactTimeAndSpace (input.map toMachineSymbol) ((f input).map toMachineSymbol) t' s'
 
 /-- The main definition of complexity of multi-tape Turing machines:
 A proof that the function `f` is computable by some multi-tape Turing machine `tm` (with finite
@@ -429,74 +351,17 @@ 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.runFrom cfg₁ t = cfg₂ := by
-  unfold runFrom
+    RelatesInSteps tm.Step cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by
   induction t generalizing cfg₁ cfg₂ with
   | zero => simp
   | succ t ih =>
-    rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply']
+    rw [RelatesInSteps.succ_iff, runFrom_succ_eq_step']
     constructor
-    · grind
+    · grind [step_iff]
     · intro h_runFrom
-      use tm.step^[t] cfg₁
-      grind
-
-/-- The Turing machine `tm` halts after exactly `t` steps on input `input`
-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.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
-    {tm : MultiTapeTM k Symbol State}
-    {input : List Symbol}
-    {t₁ t₂ : ℕ}
-    (h_halts₁ : tm.haltsAtStep input t₁)
-    (h_halts₂ : tm.haltsAtStep input t₂) :
-    t₁ = t₂ := by
-  wlog h : t₁ ≤ t₂
-  · exact (this h_halts₂ h_halts₁ (Nat.le_of_not_le h)).symm
-  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h
-  cases d with
-  | zero => rfl
-  | succ d =>
-    have halts₁ : (tm.runFrom (tm.initCfg input) t₁).state = none := by
-      simp [haltsAtStep] at h_halts₁
-      exact h_halts₁.left
-    have halts₂ : (tm.runFrom (tm.initCfg input) (d + t₁)).state ≠ none := by
-      grind [haltsAtStep, runFrom]
-    refine absurd ?_ 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.runFrom_add`. -/
-lemma not_halts_of_repeat_nonhalt
-    (cfg : Cfg k Symbol State input)
-    (h_not_halt : cfg.state ≠ none)
-    (t : ℕ)
-    (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.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.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.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.runFrom_add]
-    simp [hnh]
-  simp [hloop t', h_not_halt] at h₁
+      use tm.runFrom cfg₁ t
+      grind [step_iff]
+
 
 end MultiTapeTM
 
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
new file mode 100644
index 000000000..21b4caf37
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
@@ -0,0 +1,266 @@
+/-
+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 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 non-empty list of configurations, each reached from
+    the previous by a step, with `start` and `last` read off it
+* `ComputationPath.space_le_linear`: a machine touches at most `k` cells per step
+* `ComputationPath.single`, `ComputationPath.concat`: the runs of no steps and of one more,
+    with `ComputationPath.induction` to reason by cases on the two
+* `ComputationPath.reflTransGen`: a run reaches its last configuration from its first
+* `ComputationPath.eq_of_start_of_time`: a machine whose steps are unique has exactly one run of
+    each length from each configuration
+* `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint
+* `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`:
+    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 :=
+  c₁.StepWith c₂ fun q action => ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action
+
+/-- 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, Cfg.StepWith, 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`: the configurations it passes through, forming a
+non-empty chain of steps. Neither end is designated; `start` and `last` are read off it. -/
+structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) where
+  /-- the configurations passed through -/
+  cfgs : List (Cfg k Symbol State input)
+  /-- a run passes through at least one configuration -/
+  ne_nil : cfgs ≠ []
+  /-- consecutive configurations are joined by a step -/
+  isChain : cfgs.IsChain ntm.Step
+
+namespace ComputationPath
+
+variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol}
+
+/-- A run passes through at least one configuration. -/
+lemma length_pos (p : ntm.ComputationPath input) : 0 < p.cfgs.length :=
+  List.length_pos_iff.mpr p.ne_nil
+
+/-- The configuration the run starts from. -/
+def start (p : ntm.ComputationPath input) : Cfg k Symbol State input := p.cfgs.head p.ne_nil
+
+/-- The configuration the run ends at. -/
+def last (p : ntm.ComputationPath input) : Cfg k Symbol State input := p.cfgs.getLast p.ne_nil
+
+/-- The number of steps taken, the time the computation takes. -/
+def time (p : ntm.ComputationPath input) : ℕ := p.cfgs.length - 1
+
+/-- The number of work tape cells touched. -/
+def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.cfgs
+
+/-- A path visiting `t + 1` configurations takes `t` steps. -/
+lemma length_cfgs (p : ntm.ComputationPath input) : p.cfgs.length = p.time + 1 := by
+  have := p.length_pos
+  simp only [time]
+  omega
+
+/-- A machine touches at most `k` cells per step, whether or not it is deterministic. -/
+theorem space_le_linear (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := by
+  calc p.space ≤ k * p.cfgs.length := spaceUsedOfCfgs_le _
+    _ = k * p.time + k := by rw [p.length_cfgs, Nat.mul_succ]
+
+end ComputationPath
+
+/-- The run that does nothing. -/
+def ComputationPath.single {ntm : MultiTapeNTM k Symbol State} (c : Cfg k Symbol State input) :
+    ntm.ComputationPath input where
+  cfgs := [c]
+  ne_nil := by simp
+  isChain := by simp
+
+/-- Extend a run by one step at its end. -/
+def ComputationPath.concat (p : ntm.ComputationPath input) (c : Cfg k Symbol State input)
+    (h : ntm.Step p.last c) : ntm.ComputationPath input where
+  cfgs := p.cfgs ++ [c]
+  ne_nil := by simp
+  isChain := by
+    simpa [List.isChain_append, List.getLast?_eq_some_getLast p.ne_nil,
+      ComputationPath.last] using ⟨p.isChain, h⟩
+
+@[simp] lemma ComputationPath.single_cfgs (c : Cfg k Symbol State input) :
+    (single (ntm := ntm) c).cfgs = [c] := rfl
+
+@[simp] lemma ComputationPath.single_start (c : Cfg k Symbol State input) :
+    (single (ntm := ntm) c).start = c := rfl
+
+@[simp] lemma ComputationPath.single_last (c : Cfg k Symbol State input) :
+    (single (ntm := ntm) c).last = c := rfl
+
+@[simp] lemma ComputationPath.single_time (c : Cfg k Symbol State input) :
+    (single (ntm := ntm) c).time = 0 := rfl
+
+@[simp] lemma ComputationPath.concat_cfgs (p : ntm.ComputationPath input) (c) (h) :
+    (p.concat c h).cfgs = p.cfgs ++ [c] := rfl
+
+@[simp] lemma ComputationPath.concat_last (p : ntm.ComputationPath input) (c) (h) :
+    (p.concat c h).last = c := by simp [concat, last]
+
+@[simp] lemma ComputationPath.concat_start (p : ntm.ComputationPath input) (c) (h) :
+    (p.concat c h).start = p.start := by
+  simp [concat, start, List.head_append_of_ne_nil p.ne_nil]
+
+@[simp] lemma ComputationPath.concat_time (p : ntm.ComputationPath input) (c) (h) :
+    (p.concat c h).time = p.time + 1 := by
+  have := p.length_pos
+  simp only [concat, time, List.length_append, List.length_cons, List.length_nil]
+  omega
+
+/-- Every run is either the run of no steps, or one more step on a shorter run. This gives runs
+the induction of an inductive definition while they stay lists. -/
+@[elab_as_elim]
+theorem ComputationPath.induction {motive : ntm.ComputationPath input → Prop}
+    (single : ∀ c, motive (ComputationPath.single c))
+    (concat : ∀ (p : ntm.ComputationPath input) c h, motive p → motive (p.concat c h))
+    (p : ntm.ComputationPath input) : motive p := by
+  obtain ⟨cfgs, ne_nil, isChain⟩ := p
+  induction cfgs using List.reverseRecOn with
+  | nil => exact absurd rfl ne_nil
+  | append_singleton l a ih =>
+    rcases eq_or_ne l [] with rfl | hl
+    · exact single a
+    · have h : l.IsChain ntm.Step ∧ ntm.Step (l.getLast hl) a := by
+        simpa [List.isChain_append, List.getLast?_eq_some_getLast hl] using isChain
+      exact concat ⟨l, hl, h.1⟩ a h.2 (ih hl h.1)
+
+/-- A run witnesses that its last configuration is reachable from the one it starts at. -/
+theorem ComputationPath.reflTransGen (p : ntm.ComputationPath input) :
+    Relation.ReflTransGen ntm.Step p.start p.last := by
+  induction p using ComputationPath.induction with
+  | single c => simp only [ComputationPath.single_start, ComputationPath.single_last]
+                exact .refl
+  | concat p c h ih => simpa using ih.tail (by simpa using h)
+
+/-- A machine whose steps are unique has at most one run of a given length from a given
+configuration: the two agree configuration by configuration. -/
+theorem ComputationPath.getElem_eq
+    (hdet : ∀ {c c' c'' : Cfg k Symbol State input}, ntm.Step c c' → ntm.Step c c'' → c' = c'')
+    {p q : ntm.ComputationPath input} (hs : p.start = q.start) (i : ℕ)
+    (h₁ : i < p.cfgs.length) (h₂ : i < q.cfgs.length) : p.cfgs[i] = q.cfgs[i] := by
+  induction i with
+  | zero => simpa [ComputationPath.start, List.getElem_zero] using hs
+  | succ n ih =>
+    have hp := List.isChain_iff_getElem.mp p.isChain n h₁
+    have hq := List.isChain_iff_getElem.mp q.isChain n h₂
+    rw [ih (by omega) (by omega)] at hp
+    exact hdet hp hq
+
+/-- Such a machine has at most one run of a given length from a given configuration. -/
+theorem ComputationPath.cfgs_eq
+    (hdet : ∀ {c c' c'' : Cfg k Symbol State input}, ntm.Step c c' → ntm.Step c c'' → c' = c'')
+    {p q : ntm.ComputationPath input} (hs : p.start = q.start) (ht : p.time = q.time) :
+    p.cfgs = q.cfgs :=
+  List.ext_getElem (by rw [p.length_cfgs, q.length_cfgs, ht])
+    fun i h₁ h₂ => ComputationPath.getElem_eq hdet hs i h₁ h₂
+
+/-- Such a machine has exactly one run of a given length from a given configuration. -/
+theorem ComputationPath.eq_of_start_of_time
+    (hdet : ∀ {c c' c'' : Cfg k Symbol State input}, ntm.Step c c' → ntm.Step c c'' → c' = c'')
+    {p q : ntm.ComputationPath input} (hs : p.start = q.start) (ht : p.time = q.time) : p = q := by
+  cases p; cases q; simp_all only [ComputationPath.mk.injEq]
+  exact cfgs_eq hdet hs ht
+
+/-- `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.start = ntm.initCfg 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 ComputesInExactTime (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t : ℕ) :
+    Prop :=
+  ntm.ComputesSuchThat input output fun p => p.time = t
+
+/-- `ntm` computes `output` from `input` touching exactly `s` work tape cells. -/
+def ComputesInExactSpace (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. -/
+def ComputesInExactTimeAndSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol)
+    (t s : ℕ) : Prop :=
+  ntm.ComputesSuchThat input output fun p => p.time = 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 15145637a..5b1a5b5a3 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
@@ -16,11 +16,43 @@ This file collects lemmas about the set of positions visited by a work-tape head
 (`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.spaceUsed`) and how the tape head positions
 influence the cells that are modified on a tape.
 
+Those measures are read off the machine's own run, so results that hold of any run come from
+`MultiTapeNTM.ComputationPath` rather than being proved again here.
+
 -/
 
 @[expose] public section
 
-namespace Turing.MultiTapeTM
+namespace Turing
+
+namespace MultiTapeNTM
+
+variable {k : ℕ} {State Symbol : Type*} {input : List Symbol}
+  {ntm : MultiTapeNTM k Symbol State}
+
+/-- A work tape head moves by at most one cell in a step. -/
+lemma workTapePos_step_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) :
+    |c'.workTapePos i - c.workTapePos i| ≤ 1 := by
+  cases hq : c.state with
+  | none => simp_all [Step, Cfg.StepWith]
+  | some q =>
+    simp only [Step, Cfg.StepWith, hq] at h
+    obtain ⟨a, -, rfl⟩ := h
+    exact workTapePos_apply_le a c i
+
+/-- A step changes no work tape cell but the one its head is on. -/
+lemma workTapes_step_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (j : Fin k)
+    (z : ℤ) (hz : z ≠ c.workTapePos j) : c'.workTapes j z = c.workTapes j z := by
+  cases hq : c.state with
+  | none => simp_all [Step, Cfg.StepWith]
+  | some q =>
+    simp only [Step, Cfg.StepWith, hq] at h
+    obtain ⟨a, -, rfl⟩ := h
+    exact workTapes_apply_eq_of_ne a c j z hz
+
+end MultiTapeNTM
+
+namespace MultiTapeTM
 
 variable {k : ℕ}
 variable {State Symbol : Type*}
@@ -28,22 +60,9 @@ 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
-  unfold step
-  cases hst : cfg.state with
-  | none => simp_all
-  | some q =>
-    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.runFrom cfg t').workTapePos i = z := by
-  simp [visitedByTapeHead]
+  simp [visitedByTapeHead, visitedOfCfgs, runPath_cfgs]
 
 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 :=
@@ -52,7 +71,8 @@ lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i :
 /-- 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
-  apply Finset.image_subset_image
+  intro z hz
+  rw [mem_visitedByTapeHead] at hz ⊢
   grind
 
 /-- Starting from configuration `cfg`, every position between the initial head position of tape
@@ -62,11 +82,11 @@ lemma uIcc_workTapePos_subset_visitedByTapeHead
     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
+  | zero => simpa using tm.mem_visitedByTapeHead_self cfg 0 i
   | succ t ih =>
     intro z hz
     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
+      runFrom_succ_eq_step' (tm := tm) ▸ MultiTapeNTM.workTapePos_step_le (step_iff.mpr rfl) 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]
@@ -79,13 +99,13 @@ lemma mem_visitedByTapeHead_of_workTapes_ne
     (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
+  | zero => exact absurd (by simp) h
   | succ t ih =>
     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
+    · rw [MultiTapeNTM.workTapes_step_eq_of_ne (step_iff.mpr rfl) 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
@@ -119,18 +139,14 @@ lemma content_natAbs_le_spaceUsedByTape
 /-- The number of cells touched by a single work tape 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 := by
-  calc
-    tm.spaceUsedByTape cfg t i
-    _ ≤ (Finset.range (t + 1)).card := Finset.card_image_le
-    _ = t + 1 := Finset.card_range _
+  unfold spaceUsedByTape visitedByTapeHead visitedOfCfgs
+  exact (List.toFinset_card_le _).trans (by simp [MultiTapeNTM.ComputationPath.length_cfgs])
 
-/-- The space used by a computation is bounded linearly by the number of steps. -/
+/-- The space used by a computation is bounded linearly by the number of steps. This is
+`ComputationPath.space_le_linear` read off the machine's own run. -/
 lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) :
     tm.spaceUsed cfg t ≤ k * t + k := by
-  calc tm.spaceUsed 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]
+  simpa using (tm.runPath cfg t).space_le_linear
 
 /-- The space used by a single tape is monotone in the number of steps. -/
 lemma spaceUsedByTape_mono
@@ -145,6 +161,9 @@ lemma spaceUsedByTape_mono
 lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) :
     Monotone (tm.spaceUsed cfg ·) := by
   intro t t' h
-  exact Finset.sum_le_sum (fun i _ => spaceUsedByTape_mono tm cfg i h)
+  simp only [spaceUsed_eq_spaceUsedOfCfgs]
+  exact spaceUsedOfCfgs_mono ((List.range_sublist.mpr (by omega)).map _)
+
+end MultiTapeTM
 
-end Turing.MultiTapeTM
+end Turing