diff --git a/Cslib.lean b/Cslib.lean
index 34a0d27bef..3a80ee7e10 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -47,6 +47,9 @@ 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.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
 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/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 94a6024895..8739d5cc68 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
@@ -293,6 +293,20 @@ 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]
 
+/-- Once a run has halted, every later time denotes the same configuration. -/
+lemma runFrom_eq_of_halt (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)
+    (hhalt : (tm.runFrom cfg τ).state = none) :
+    tm.runFrom cfg t = tm.runFrom cfg τ := by
+  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hle
+  rw [runFrom_add, runFrom_of_halt _ hhalt]
+
+/-- Halting is monotone in the number of execution steps. -/
+lemma runFrom_state_eq_none_mono (cfg : Cfg k Symbol State input) :
+    Monotone fun t => (tm.runFrom cfg t).state = none := by
+  intro τ t hle hhalt
+  rw [runFrom_eq_of_halt cfg hle hhalt]
+  exact hhalt
+
 @[simp]
 lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) :
     tm.outputSymbol cfg = none := by
@@ -368,9 +382,28 @@ 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]
+    (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output :=
+  congrArg Cfg.output (tm.runFrom_eq_of_halt cfg hle hhalt)
+
+/-- Output length is monotone because a machine only appends output symbols. -/
+lemma runFrom_output_length_mono
+    (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) :
+    Monotone fun t => (tm.runFrom cfg t).output.length := by
+  apply monotone_nat_of_le_succ
+  intro t
+  rw [runFrom_succ_eq_step', step_output, List.length_append]
+  exact Nat.le_add_right _ _
+
+/-- A run can append at most one output symbol per step. -/
+lemma runFrom_output_length_le
+    (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.runFrom cfg t).output.length ≤ cfg.output.length + t := by
+  induction t with
+  | zero => simp
+  | succ t ih =>
+      rw [runFrom_succ_eq_step', step_output, List.length_append]
+      grind [Option.toList]
 
 /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps
 and uses exactly `s` space.
@@ -383,6 +416,15 @@ def ComputesInTimeAndSpace
   (tm.runFrom (tm.initCfg input) t).output = output ∧
   tm.spaceUsed (tm.initCfg input) t = s
 
+/-- The output of a computation is no longer than its running time. -/
+lemma output_length_le_time
+    {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ}
+    (h : ComputesInTimeAndSpace tm input output t s) :
+    output.length ≤ t := by
+  obtain ⟨-, hout, -⟩ := h
+  rw [← hout]
+  simpa using tm.runFrom_output_length_le (tm.initCfg input) t
+
 /-- A machine computes `f` between the supplied encodings, with bounds depending on the input.
 The machine's alphabet and state type need not be finite. -/
 def ComputesFunInTimeAndSpace {α β : Type*}
@@ -457,35 +499,40 @@ lemma relatesInSteps_iff_runFrom_eq
       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₁
+/-- The run from `cfg` first reaches a halting configuration at time `t`.
+An already halted starting configuration has halting time zero. -/
+structure HaltsAt (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input)
+    (t : ℕ) : Prop where
+  /-- The configuration at time `t` is halted. -/
+  halted : (tm.runFrom cfg t).state = none
+  /-- All earlier configurations are active. -/
+  active : ∀ s < t, (tm.runFrom cfg s).state ≠ none
+
+/-- A run has at most one first halting time. -/
+lemma HaltsAt.unique {tm : MultiTapeTM k Symbol State} {cfg : Cfg k Symbol State input}
+    {t₀ t₁ : ℕ} (h₀ : tm.HaltsAt cfg t₀) (h₁ : tm.HaltsAt cfg t₁) : t₀ = t₁ := by
+  rcases lt_trichotomy t₀ t₁ with h | h | h
+  · exact (h₁.active t₀ h h₀.halted).elim
+  · exact h
+  · exact (h₀.active t₁ h h₁.halted).elim
+
+/-- The machine first halts at step `t` when started on `input`. -/
+abbrev haltsAtStep (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : Prop :=
+  tm.HaltsAt (tm.initCfg input) t
+
+/-- Every halted run has a first halting time no later than the supplied time. -/
+lemma exists_minimal_halting_time (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) (t : ℕ)
+    (hhalt : (tm.runFrom cfg t).state = none) :
+    ∃ s ≤ t, tm.HaltsAt cfg s := by
+  let hExists : ∃ n, (tm.runFrom cfg n).state = none := ⟨t, hhalt⟩
+  exact ⟨Nat.find hExists, Nat.find_min' hExists hhalt, Nat.find_spec hExists,
+    fun _ hs => Nat.find_min hExists hs⟩
+
+/-- If a Turing machine halts, its first halting step is unique. -/
+lemma halting_step_unique {tm : MultiTapeTM k Symbol State} {input : List Symbol}
+    {t₀ t₁ : ℕ} (h₀ : tm.haltsAtStep input t₀) (h₁ : tm.haltsAtStep input t₁) :
+    t₀ = t₁ := h₀.unique h₁
 
 /-- If a deterministic machine repeats a non-halting configuration, it never halts,
 because the sequence between the two configurations will loop forever.
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean
new file mode 100644
index 0000000000..9199d84089
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-! # Configuration state replacement and execution paths
+
+`Cfg.withState` changes the control state, possibly changing its type, and preserves all tapes,
+head positions, and accumulated output. `runFrom_map` transports runs along maps that preserve
+steps, and `runFrom_eq_of_isChain` identifies the endpoint of an explicit execution path.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {State Symbol : Type*} {input : List Symbol}
+
+/-- The configuration `cfg` with its state replaced by `q`, possibly over a different state
+type. -/
+@[simps]
+def Cfg.withState (cfg : Cfg k Symbol State input) {State' : Type*}
+    (q : Option State') : Cfg k Symbol State' input :=
+  ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
+
+@[simp]
+lemma Cfg.withState_inputSymbol {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).inputSymbol = cfg.inputSymbol := rfl
+
+@[simp]
+lemma Cfg.withState_workTapeSymbols {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).workTapeSymbols = cfg.workTapeSymbols := rfl
+
+@[simp]
+lemma Cfg.withState_withState {cfg : Cfg k Symbol State input} {State' State'' : Type*}
+    {q : Option State'} {q' : Option State''} :
+    (cfg.withState q).withState q' = cfg.withState q' := rfl
+
+@[simp]
+lemma Cfg.withState_self {cfg : Cfg k Symbol State input} :
+    cfg.withState cfg.state = cfg := rfl
+
+/-- A map that preserves steps maps every configuration of an execution. -/
+lemma runFrom_map {k' : ℕ} {Symbol' State' : Type*} {input' : List Symbol'}
+    (tm : MultiTapeTM k Symbol State) (tm' : MultiTapeTM k' Symbol' State')
+    (embed : Cfg k Symbol State input → Cfg k' Symbol' State' input')
+    (hstep : ∀ cfg, tm'.step (embed cfg) = embed (tm.step cfg))
+    (cfg : Cfg k Symbol State input) (n : ℕ) :
+    tm'.runFrom (embed cfg) n = embed (tm.runFrom cfg n) := by
+  have h : Function.Semiconj embed tm.step tm'.step := fun cfg => (hstep cfg).symm
+  exact (h.iterate_right n cfg).symm
+
+/-- An execution path ends at the configuration reached after one step per adjacent pair. -/
+lemma runFrom_eq_of_isChain (tm : MultiTapeTM k Symbol State)
+    {cfg cfg' : Cfg k Symbol State input} {path : List (Cfg k Symbol State input)}
+    (hpath : path.IsChainFromTo tm.TransitionRelation cfg cfg') :
+    tm.runFrom cfg (path.length - 1) = cfg' := by
+  apply (tm.relatesInSteps_iff_runFrom_eq cfg cfg' _).mp
+  exact hpath.relatesInSteps (by have := hpath.length_pos; omega)
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean
new file mode 100644
index 0000000000..739347426f
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+public import Mathlib.Data.Fintype.Inv
+public import Mathlib.Data.Fintype.Card
+
+/-!
+# Extending and reindexing work tapes
+
+`extendTapes` embeds a machine's work tapes along an injection. The extra tapes are idle, and each
+native step still takes exactly one step. The configuration embedding permits arbitrary contents
+and head positions on the extra tapes, so the transformation also applies to intermediate runs.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k k' : ℕ} {Symbol State : Type*} {input : List Symbol}
+
+namespace ExtendTapes
+
+/-- Extend a tape-indexed family along an injection, using `extra` outside its image. -/
+def extend {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) (extra : Fin k' → α)
+    (j : Fin k') : α :=
+  if h : j ∈ Set.range e then values (e.invOfMemRange ⟨j, h⟩) else extra j
+
+@[simp]
+lemma extend_apply {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α)
+    (extra : Fin k' → α) (i : Fin k) : extend e values extra (e i) = values i := by
+  simp [extend]
+
+/-- Embed a native configuration while retaining arbitrary data on the unused tapes. -/
+def embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input)
+    (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) :
+    Cfg k' Symbol State input where
+  state := cfg.state
+  inputPos := cfg.inputPos
+  workTapes := extend e cfg.workTapes extraTapes
+  workTapePos := extend e cfg.workTapePos extraPos
+  output := cfg.output
+
+end ExtendTapes
+
+/-- Relabel the work tapes by an injection, leaving every tape outside its image idle. -/
+def extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') :
+    MultiTapeTM k' Symbol State where
+  q₀ := tm.q₀
+  tr q input work :=
+    let action := tm.tr q input (work ∘ e)
+    ⟨action.inputMove, ExtendTapes.extend e action.workActions (fun _ => (none, 0)),
+      action.outS, action.q'⟩
+
+namespace ExtendTapes
+
+variable (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k')
+variable (cfg : Cfg k Symbol State input)
+variable (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ)
+
+/-- Tape extension preserves a step and every unused tape. -/
+lemma step_embed :
+    (tm.extendTapes e).step (embed e cfg extraTapes extraPos) =
+      embed e (tm.step cfg) extraTapes extraPos := by
+  have hwork : (embed e cfg extraTapes extraPos).workTapeSymbols ∘ e = cfg.workTapeSymbols := by
+    funext i
+    simp [embed, Cfg.workTapeSymbols]
+  cases hs : cfg.state with
+  | none => simp [step, embed, hs]
+  | some q =>
+    simp only [step, embed, hs, extendTapes, Cfg.inputSymbol] at hwork ⊢
+    rw [hwork]
+    apply Cfg.ext <;> try rfl
+    · funext j p
+      by_cases hj : j ∈ Set.range e
+      · obtain ⟨i, rfl⟩ := hj
+        simp [extend_apply]
+      · simp [extend, hj]
+    · funext j
+      by_cases hj : j ∈ Set.range e
+      · obtain ⟨i, rfl⟩ := hj
+        simp [extend_apply]
+      · simp [extend, hj]
+
+/-- Tape extension maps each configuration of the native run, preserving the unused tapes. -/
+lemma runFrom_embed (n : ℕ) :
+    (tm.extendTapes e).runFrom (embed e cfg extraTapes extraPos) n =
+      embed e (tm.runFrom cfg n) extraTapes extraPos :=
+  runFrom_map tm (tm.extendTapes e) (fun cfg => embed e cfg extraTapes extraPos)
+    (fun cfg => step_embed tm e cfg extraTapes extraPos) cfg n
+
+/-- An injected tape visits exactly the native tape's positions. -/
+lemma spaceUsedByTape_embed (n : ℕ) (i : Fin k) :
+    (tm.extendTapes e).spaceUsedByTape (embed e cfg extraTapes extraPos) n (e i) =
+      tm.spaceUsedByTape cfg n i := by
+  simp only [spaceUsedByTape, visitedByTapeHead, runFrom_embed]
+  simp only [embed, extend_apply]
+
+/-- An unused tape visits just its initial cell. -/
+lemma spaceUsedByTape_extra (n : ℕ) (j : Fin k') (hj : j ∉ Set.range e) :
+    (tm.extendTapes e).spaceUsedByTape (embed e cfg extraTapes extraPos) n j = 1 := by
+  simp only [spaceUsedByTape, visitedByTapeHead, runFrom_embed]
+  simp [embed, extend, hj, Finset.image_const]
+
+/-- The extra space is exactly one visited cell for each unused tape. -/
+lemma spaceUsed_embed (n : ℕ) :
+    (tm.extendTapes e).spaceUsed (embed e cfg extraTapes extraPos) n =
+      tm.spaceUsed cfg n + (k' - k) := by
+  unfold spaceUsed
+  rw [← Finset.sum_add_sum_compl (Finset.univ.map e)]
+  congr 1
+  · simp [Finset.sum_map, spaceUsedByTape_embed]
+  · calc
+      _ = ∑ j ∈ (Finset.univ.map e)ᶜ, 1 := by
+        apply Finset.sum_congr rfl
+        intro j hj
+        exact spaceUsedByTape_extra tm e cfg extraTapes extraPos n j (by simpa using hj)
+      _ = k' - k := by simp [Finset.card_compl]
+
+end ExtendTapes
+
+/-- Starting with blank work tapes commutes with tape extension. -/
+lemma runFrom_extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k')
+    (input : List Symbol) (n : ℕ) :
+    (tm.extendTapes e).runFrom ((tm.extendTapes e).initCfg input) n =
+      ExtendTapes.embed e (tm.runFrom (tm.initCfg input) n) (fun _ _ => none) (fun _ => 0) := by
+  have hinit : (tm.extendTapes e).initCfg input =
+      ExtendTapes.embed e (tm.initCfg input) (fun _ _ => none) (fun _ => 0) := by
+    ext i p <;> simp [ExtendTapes.embed, ExtendTapes.extend, extendTapes]
+  rw [hinit, ExtendTapes.runFrom_embed]
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md
new file mode 100644
index 0000000000..1f0d320eef
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md
@@ -0,0 +1,11 @@
+# Machine transformations
+
+These modules describe executable machines and their effects on configurations and `runFrom`.
+
+- `Basic` changes a configuration's control state without changing its tapes, transports runs
+  along maps that preserve steps, and relates explicit execution paths to `runFrom`.
+- `Sequential` runs machines with the same work-tape count consecutively. The first halting
+  transition hands its tapes, head positions, and accumulated output to the second machine,
+  which starts in its own fixed initial state.
+- `ExtendTapes` places a machine's tapes along any injection. Time is unchanged; each unused tape
+  contributes one visited cell to space. Arbitrary data on unused tapes is preserved.
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean
new file mode 100644
index 0000000000..c5a03ee6bd
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+
+/-!
+# Sequential execution on shared tapes
+
+`seq` runs two machines with the same work-tape count. The transition that would halt the first
+machine instead enters the second machine's initial state. Tape contents, head positions, and
+accumulated output are carried across, with no extra transition for the handoff. No information
+is passed through the finite control state: the second machine starts in its own initial state.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State State₀ State₁ : Type*} {input : List Symbol}
+
+/-- Run two machines sequentially on the same tapes, handing off on the first halting transition. -/
+def seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) :
+    MultiTapeTM k Symbol (State₀ ⊕ State₁) where
+  q₀ := .inl tm₀.q₀
+  tr q input work := match q with
+    | .inl q =>
+      let action := tm₀.tr q input work
+      ⟨action.inputMove, action.workActions, action.outS,
+        some (action.q'.elim (.inr tm₁.q₀) Sum.inl)⟩
+    | .inr q =>
+      let action := tm₁.tr q input work
+      ⟨action.inputMove, action.workActions, action.outS, action.q'.map Sum.inr⟩
+
+namespace Sequential
+
+/-- A first-machine configuration; a native halt becomes the second machine's initial state. -/
+def left (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) :
+    Cfg k Symbol (State₀ ⊕ State₁) input :=
+  cfg.withState (some (cfg.state.elim (.inr tm₁.q₀) Sum.inl))
+
+/-- A second-machine configuration, including a final halt. -/
+def right (cfg : Cfg k Symbol State₁ input) : Cfg k Symbol (State₀ ⊕ State₁) input :=
+  cfg.withState (cfg.state.map Sum.inr)
+
+variable (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁)
+
+/-- The left embedding preserves each step before the native halt. -/
+lemma step_left (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) :
+    (seq tm₀ tm₁).step (left tm₁ cfg) = left tm₁ (tm₀.step cfg) := by
+  cases hs : cfg.state with
+  | none => exact (h hs).elim
+  | some q =>
+    simp only [step, left, Cfg.withState, seq, hs, Option.elim_some]
+    rfl
+
+/-- The right embedding preserves every step, including steps after halting. -/
+lemma step_right (cfg : Cfg k Symbol State₁ input) :
+    (seq tm₀ tm₁).step (right cfg) = right (tm₁.step cfg) := by
+  cases hs : cfg.state <;>
+    simp only [step, right, Cfg.withState, seq, hs, Option.map_some, Option.map_none]
+  rfl
+
+/-- The first run is preserved up to its earliest halt. -/
+lemma runFrom_left (cfg : Cfg k Symbol State₀ input) (n : ℕ)
+    (h : ∀ m < n, (tm₀.runFrom cfg m).state ≠ none) :
+    (seq tm₀ tm₁).runFrom (left tm₁ cfg) n = left tm₁ (tm₀.runFrom cfg n) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [runFrom_succ_eq_step', ih (fun m hm => h m (by omega)),
+      step_left tm₀ tm₁ _ (h n (by omega)), runFrom_succ_eq_step']
+
+/-- Once in the second phase, runs are exactly the second machine's runs. -/
+lemma runFrom_right (cfg : Cfg k Symbol State₁ input) (n : ℕ) :
+    (seq tm₀ tm₁).runFrom (right cfg) n = right (tm₁.runFrom cfg n) :=
+  runFrom_map tm₁ (seq tm₀ tm₁) right (step_right tm₀ tm₁) cfg n
+
+end Sequential
+
+/-- Sequential execution splits at the first machine's earliest halt. The second machine receives
+all final tapes and head positions, together with the output accumulated so far. -/
+lemma runFrom_seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁)
+    (cfg : Cfg k Symbol State₀ input) (u v : ℕ)
+    (hhalt : tm₀.HaltsAt cfg u) :
+    (seq tm₀ tm₁).runFrom (Sequential.left tm₁ cfg) (u + v) =
+      Sequential.right (tm₁.runFrom ((tm₀.runFrom cfg u).withState (some tm₁.q₀)) v) := by
+  rw [runFrom_add, Sequential.runFrom_left tm₀ tm₁ cfg u hhalt.active]
+  rw [show Sequential.left tm₁ (tm₀.runFrom cfg u) =
+    Sequential.right ((tm₀.runFrom cfg u).withState (some tm₁.q₀)) by
+      simp [Sequential.left, Sequential.right, Cfg.withState, hhalt.halted]]
+  exact Sequential.runFrom_right tm₀ tm₁ _ v
+
+end Turing.MultiTapeTM
diff --git a/CslibTests.lean b/CslibTests.lean
index 4e3f3f3a46..2c6af5ae9b 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -19,5 +19,6 @@ import CslibTests.Modal
 import CslibTests.Modal.Ideal
 import CslibTests.Modal.Stlc
 import CslibTests.MultiTapeComplexity
+import CslibTests.MultiTapePlumbing
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/MultiTapePlumbing.lean b/CslibTests/MultiTapePlumbing.lean
new file mode 100644
index 0000000000..067b0b3f2a
--- /dev/null
+++ b/CslibTests/MultiTapePlumbing.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes
+
+namespace CslibTests.MultiTapePlumbing
+
+open Turing.MultiTapeTM
+
+private def finish (move : SignType) (symbol : Bool) : Turing.MultiTapeTM 0 Bool Unit where
+  q₀ := ()
+  tr _ _ _ := ⟨move, Fin.elim0, some symbol, none⟩
+
+-- Sequential execution retains the output accumulated by the first machine.
+example : (((finish 0 true).seq (finish 0 false)).runFrom
+    (((finish 0 true).seq (finish 0 false)).initCfg []) 2).output = [true, false] := by rfl
+
+private def sparse : Fin 1 ↪ Fin 3 := ⟨fun _ => 2, fun _ _ _ => Subsingleton.elim _ _⟩
+
+private def writer : Turing.MultiTapeTM 1 Bool Unit where
+  q₀ := ()
+  tr _ _ _ := ⟨0, fun _ => (some (some true), 1), none, none⟩
+
+-- The injection is not an initial-segment inclusion; unused tape data and heads are retained.
+example : ((writer.extendTapes sparse).runFrom
+    (ExtendTapes.embed sparse (writer.initCfg [])
+      (fun _ _ => some false) (fun _ => 7)) 1).workTapes 0 0 = some false := by rfl
+
+example : ((writer.extendTapes sparse).runFrom
+    (ExtendTapes.embed sparse (writer.initCfg [])
+      (fun _ _ => some false) (fun _ => 7)) 1).workTapePos 0 = 7 := by rfl
+
+example : ((writer.extendTapes sparse).runFrom
+    (ExtendTapes.embed sparse (writer.initCfg [])
+      (fun _ _ => some false) (fun _ => 7)) 1).workTapes 2 0 = some true := by rfl
+
+-- Exact halting time includes an already halted starting configuration.
+example (cfg : Cfg 0 Bool Unit []) (h : cfg.state = none) :
+    (finish 0 true).HaltsAt cfg 0 :=
+  ⟨h, fun _ hs => (Nat.not_lt_zero _ hs).elim⟩
+
+-- An initialized machine must take a step before halting; later padded times are not first halts.
+example : ¬ (finish 0 true).haltsAtStep [] 0 := by
+  intro h
+  simpa [runFrom, initCfg] using h.halted
+
+example : (finish 0 true).haltsAtStep [] 1 := by
+  refine ⟨rfl, ?_⟩
+  intro s hs
+  have : s = 0 := by omega
+  subst s
+  simp [runFrom, initCfg]
+
+example : ¬ (finish 0 true).haltsAtStep [] 2 := by
+  intro h
+  exact h.active 1 (by decide) rfl
+
+-- A zero-time first phase hands off without charging an additional step.
+example (cfg : Cfg 0 Bool Unit []) (h : cfg.state = none) :
+    ((finish 0 true).seq (finish 0 false)).runFrom
+        (Sequential.left (finish 0 false) cfg) 1 =
+      Sequential.right ((finish 0 false).step (cfg.withState (some ()))) :=
+  runFrom_seq _ _ cfg 0 1 ⟨h, fun _ hs => (Nat.not_lt_zero _ hs).elim⟩
+
+end CslibTests.MultiTapePlumbing