diff --git a/Cslib.lean b/Cslib.lean
index 34a0d27bef..addf55bcec 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -46,7 +46,23 @@ 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.Combinators.AlmostConstant
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Concat
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Ite
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Tuple
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.While
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option
+public import Cslib.Computability.Machines.Turing.MultiTape.Encodings.Pair
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Clean
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.LiftTapes
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OnTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Words
 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/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 644d181d18..5e8e4d2fb2 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -13,7 +13,6 @@ public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 public import Mathlib.SetTheory.Cardinal.NatCard
-public import Mathlib.Data.Finite.Sigma
 public import Mathlib.Logic.Equiv.Fin.Basic
 
 /-!
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index 6f702d31f8..ae70a9fee4 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -16,7 +16,7 @@ public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.DA.ToNA
 public import Mathlib.Computability.DFA
 public import Mathlib.Computability.RegularExpressions
-public import Mathlib.Data.Finite.Sum
+public import Mathlib.Basic.Finite.Sum
 public import Mathlib.Data.Set.Card
 
 /-!
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/AlmostConstant.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/AlmostConstant.lean
new file mode 100644
index 0000000000..1e091322b6
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/AlmostConstant.lean
@@ -0,0 +1,391 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Data.List.Infix
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Complexity of Almost Constant Functions
+
+A function `f : α → β` that is constant except for a finite number of arguments is computable in
+constant time and zero space: the machine reads the encoded input while remembering the prefix it
+has seen so far. After a finite number of steps it either reaches the end of the input or a point
+where the prefix cannot be extended to the encoding of one of the finitely many exceptions. In both
+cases, it emits the corresponding output one symbol at a time.
+
+This result also holds for functions whose domain is already finite.
+
+## Main Results
+
+* `computableInTimeAndSpace_of_finite`: Every function on a finite type is computable in
+    constant time and zero space, relative to any encoding.
+* `computableInTimeAndSpace_of_exists_finite_ne`: Every function that is constant except
+    for a finite number of arguments is computable in constant time and zero space, relative to any
+    encoding.
+* `computableInTimeAndSpace_of_const`: Every constant function is computable in constant
+    time and zero space, relative to any encoding.
+* `computableInTimeAndSpace_almostConstTime` and
+    `computableInTimeAndSpace_finiteFunTime`: The same with explicit time bounds.
+
+-/
+
+namespace Turing.MultiTapeTM
+
+section AlmostConstFun
+
+/-! ## The machine computing a function that is constant outside a finite set
+
+The machine `almostConstTM encIn encOut f S out` computes `f`, provided that the encoded output
+of `f` is the fixed Boolean string `out` outside of the finite set `S`. -/
+
+variable {α β : Type*} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β}
+  {S : Finset α} {out : List Bool}
+
+/-- The prefixes of the encodings of the elements of a finite set `S`, together with the empty list.
+
+The empty list has to be added explicitly for the case where `S` is empty: `almostConstTM` uses
+the elements of this set as its states while reading the input, so the set has to contain the
+starting state `[]` even if there is nothing to distinguish. -/
+def encPrefixes (encIn : α ↪ List Bool) (S : Finset α) : Finset (List Bool) :=
+  insert [] (S.biUnion fun a => (encIn a).inits.toFinset)
+
+lemma mem_encPrefixes {p : List Bool} {a : α} (ha : a ∈ S) (h : p <+: encIn a) :
+    p ∈ encPrefixes encIn S := by
+  simp only [encPrefixes, Finset.mem_insert, Finset.mem_biUnion, List.mem_toFinset, List.mem_inits]
+  exact Or.inr ⟨a, ha, h⟩
+
+/-- The set of prefixes is closed under taking prefixes. -/
+lemma prefix_mem_encPrefixes {p q : List Bool} (h : p ∈ encPrefixes encIn S) (hq : q <+: p) :
+    q ∈ encPrefixes encIn S := by
+  simp only [encPrefixes, Finset.mem_insert, Finset.mem_biUnion, List.mem_toFinset,
+    List.mem_inits] at h ⊢
+  rcases h with rfl | ⟨a, ha, hp⟩
+  · exact Or.inl (List.prefix_nil.mp hq)
+  · exact Or.inr ⟨a, ha, hq.trans hp⟩
+
+/-- The suffixes of the default output and of the encoded values of `f` on `S`. -/
+def outSuffixes (encOut : β ↪ List Bool) (f : α → β) (S : Finset α) (out : List Bool) :
+    Finset (List Bool) :=
+  out.tails.toFinset ∪ S.biUnion fun a => (encOut (f a)).tails.toFinset
+
+lemma suffix_out_mem_outSuffixes {w : List Bool} (h : w <:+ out) :
+    w ∈ outSuffixes encOut f S out := by
+  simp only [outSuffixes, Finset.mem_union, List.mem_toFinset, List.mem_tails]
+  exact Or.inl h
+
+lemma mem_outSuffixes {w : List Bool} {a : α} (ha : a ∈ S) (h : w <:+ encOut (f a)) :
+    w ∈ outSuffixes encOut f S out := by
+  simp only [outSuffixes, Finset.mem_union, Finset.mem_biUnion, List.mem_toFinset, List.mem_tails]
+  exact Or.inr ⟨a, ha, h⟩
+
+/-- The set of suffixes is closed under taking suffixes. -/
+lemma suffix_mem_outSuffixes {v w : List Bool} (h : w ∈ outSuffixes encOut f S out) (hv : v <:+ w) :
+    v ∈ outSuffixes encOut f S out := by
+  simp only [outSuffixes, Finset.mem_union, Finset.mem_biUnion, List.mem_toFinset,
+    List.mem_tails] at h ⊢
+  rcases h with h | ⟨a, ha, h⟩
+  · exact Or.inl (hv.trans h)
+  · exact Or.inr ⟨a, ha, hv.trans h⟩
+
+lemma tail_mem_outSuffixes {w : List Bool} (h : w ∈ outSuffixes encOut f S out) :
+    w.tail ∈ outSuffixes encOut f S out :=
+  suffix_mem_outSuffixes h (List.tail_suffix w)
+
+/-- If the encoded output is the default output outside of `S`, then every encoded output occurs
+among the suffixes. -/
+lemma encOut_mem_outSuffixes (h : ∀ a ∉ S, encOut (f a) = out) (a : α) :
+    encOut (f a) ∈ outSuffixes encOut f S out := by
+  by_cases ha : a ∈ S
+  · exact mem_outSuffixes ha (List.suffix_refl _)
+  · rw [h a ha]
+    exact suffix_out_mem_outSuffixes (List.suffix_refl _)
+
+/-- The states of the machine `almostConstTM`: either the prefix of the input read so far, or the
+part of the output that still has to be emitted. -/
+abbrev AlmostConstState (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β)
+    (S : Finset α) (out : List Bool) : Type :=
+  {p : List Bool // p ∈ encPrefixes encIn S} ⊕ {w : List Bool // w ∈ outSuffixes encOut f S out}
+
+open Classical in
+/-- The function `f`, transported along the encodings of its domain and codomain: it maps the
+encoding of an element of `S` to the encoding of its value under `f`, and every other list to the
+default output. -/
+noncomputable def encodedFun (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β)
+    (S : Finset α) (out : List Bool) (p : List Bool) : List Bool :=
+  if h : ∃ a ∈ S, encIn a = p then encOut (f h.choose) else out
+
+@[simp]
+lemma encodedFun_enc {a : α} (ha : a ∈ S) :
+    encodedFun encIn encOut f S out (encIn a) = encOut (f a) := by
+  have hex : ∃ a' ∈ S, encIn a' = encIn a := ⟨a, ha, rfl⟩
+  rw [encodedFun, dite_eq_left_of_eq_true (eq_true hex), encIn.injective hex.choose_spec.2]
+
+@[simp]
+lemma encodedFun_enc_of_notMem {a : α} (ha : a ∉ S) :
+    encodedFun encIn encOut f S out (encIn a) = out := by
+  have hex : ¬ ∃ a' ∈ S, encIn a' = encIn a := by
+    rintro ⟨a', ha', h⟩
+    exact ha (encIn.injective h ▸ ha')
+  rw [encodedFun, dite_eq_right_of_eq_false (eq_false hex)]
+
+lemma encodedFun_mem_outSuffixes (p : List Bool) :
+    encodedFun encIn encOut f S out p ∈ outSuffixes encOut f S out := by
+  rw [encodedFun]
+  split
+  · next h => exact mem_outSuffixes h.choose_spec.1 (List.suffix_refl _)
+  · exact suffix_out_mem_outSuffixes (List.suffix_refl _)
+
+open Classical in
+/-- The machine computing a function that is constant outside of `S`. It has no work tapes.
+
+While reading the input it remembers the prefix read so far. Once this prefix cannot be extended
+to the encoding of an element of `S` anymore, or the blank behind the input is reached, it
+switches to the state that holds the encoded output, which it then emits one symbol per step
+before halting. -/
+noncomputable def almostConstTM (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β)
+    (S : Finset α) (out : List Bool) :
+    MultiTapeTM 0 Bool (AlmostConstState encIn encOut f S out) where
+  q₀ := Sum.inl ⟨[], by simp [encPrefixes]⟩
+  tr q input _ :=
+    match q with
+    | Sum.inl p =>
+      match input with
+      | some b =>
+        if h : p.val ++ [b] ∈ encPrefixes encIn S then
+          ⟨.pos, Fin.elim0, none, some (Sum.inl ⟨p.val ++ [b], h⟩)⟩
+        else
+          ⟨0, Fin.elim0, none,
+            some (Sum.inr ⟨out, suffix_out_mem_outSuffixes (List.suffix_refl out)⟩)⟩
+      | none =>
+        ⟨0, Fin.elim0, none,
+          some (Sum.inr ⟨encodedFun encIn encOut f S out p.val,
+            encodedFun_mem_outSuffixes p.val⟩)⟩
+    | Sum.inr w =>
+      ⟨0, Fin.elim0, w.val.head?,
+        if w.val = [] then none
+        else some (Sum.inr ⟨w.val.tail, tail_mem_outSuffixes w.property⟩)⟩
+
+/-- The configuration reached after `j` steps of reading the input. -/
+lemma runFrom_read (a : α) {j : ℕ} (hj : j ≤ (encIn a).length)
+    (hmem : (encIn a).take j ∈ encPrefixes encIn S) :
+    (almostConstTM encIn encOut f S out).runFrom
+        ((almostConstTM encIn encOut f S out).initCfg (encIn a)) j =
+      { state := some (Sum.inl ⟨(encIn a).take j, hmem⟩),
+        inputPos := ⟨1 + j, by omega⟩,
+        workTapes := fun _ _ => none,
+        workTapePos := fun _ => 0,
+        output := [] } := by
+  induction j with
+  | zero =>
+    simp only [runFrom_zero, initCfg, List.take_zero]
+    ext <;> simp [almostConstTM]
+  | succ j ih =>
+    have hprefix : (encIn a).take j <+: (encIn a).take (j + 1) := by
+      simp
+    have hmem' : (encIn a).take j ∈ encPrefixes encIn S := prefix_mem_encPrefixes hmem hprefix
+    have hcat : (encIn a).take j ++ [(encIn a)[j]] ∈ encPrefixes encIn S := by
+      grind [List.take_concat_get']
+    have hmove : moveInputPos (⟨1 + j, by omega⟩ : Fin ((encIn a).length + 2)) SignType.pos
+        = ⟨1 + (j + 1), by omega⟩ := by
+      grind [moveInputPos_pos_of_ne_right]
+    have hstart : 1 + j ≠ 0 := by omega
+    have hend : 1 + j ≠ (encIn a).length + 1 := by omega
+    have hprev : 1 + j - 1 = j := by omega
+    rw [runFrom_succ_eq_step', ih (by omega) hmem']
+    simp only [step, almostConstTM, Cfg.inputSymbol, Fin.ext_iff, Fin.val_zero, hstart, hend,
+      hprev, reduceDIte, hcat]
+    exact Cfg.ext_zero_tapes (by grind [List.take_concat_get']) hmove (by simp)
+
+/-- The configuration reached after having emitted the first `i` symbols of `w`, starting from a
+configuration that is about to emit `w`. -/
+lemma runFrom_write {input : List Bool} (pos : Fin (input.length + 2)) (o : List Bool)
+    {w : List Bool} (hw : w ∈ outSuffixes encOut f S out) {i : ℕ} (hi : i ≤ w.length) :
+    (almostConstTM encIn encOut f S out).runFrom
+        { state := some (Sum.inr ⟨w, hw⟩), inputPos := pos, workTapes := fun _ _ => none,
+          workTapePos := fun _ => 0, output := o } i =
+      { state := some (Sum.inr ⟨w.drop i, suffix_mem_outSuffixes hw (w.drop_suffix i)⟩),
+        inputPos := pos,
+        workTapes := fun _ _ => none,
+        workTapePos := fun _ => 0,
+        output := o ++ w.take i } := by
+  induction i with
+  | zero => simp [runFrom_zero]
+  | succ i ih =>
+    have hilt : i < w.length := by omega
+    have htake := List.take_concat_get' w i hilt
+    have hnotdone : ¬ (w.length ≤ i) := by omega
+    rw [runFrom_succ_eq_step', ih (by omega)]
+    simp only [step, almostConstTM, List.head?_drop, List.getElem?_eq_getElem hilt,
+      List.drop_eq_nil_iff, hnotdone, reduceIte, List.tail_drop, moveInputPos_zero,
+      Option.toList_some]
+    exact Cfg.ext_zero_tapes rfl rfl (by grind)
+
+/-- Starting from a configuration that is about to emit `w`, the machine halts after `w.length + 1`
+steps, having emitted `w`. -/
+lemma runFrom_write_halted {input : List Bool} (pos : Fin (input.length + 2)) (o : List Bool)
+    {w : List Bool} (hw : w ∈ outSuffixes encOut f S out) :
+    (almostConstTM encIn encOut f S out).runFrom
+        { state := some (Sum.inr ⟨w, hw⟩), inputPos := pos, workTapes := fun _ _ => none,
+          workTapePos := fun _ => 0, output := o } (w.length + 1) =
+      { state := none,
+        inputPos := pos,
+        workTapes := fun _ _ => none,
+        workTapePos := fun _ => 0,
+        output := o ++ w } := by
+  rw [runFrom_succ_eq_step', runFrom_write pos o hw le_rfl]
+  simp only [step, almostConstTM, List.drop_length, reduceIte, List.head?_nil, moveInputPos_zero,
+    Option.toList_none, List.append_nil, List.take_length]
+  exact Cfg.ext_zero_tapes rfl rfl (by simp)
+
+/-- A constant time bound for the machine `almostConstTM`. -/
+public def almostConstTime (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β)
+    (S : Finset α) (out : List Bool) : ℕ :=
+  2 + out.length + S.sup fun a => (encIn a).length + (encOut (f a)).length
+
+lemma length_le_sup_of_mem_encPrefixes {p : List Bool} (h : p ∈ encPrefixes encIn S) :
+    p.length ≤ S.sup fun a => (encIn a).length + (encOut (f a)).length := by
+  simp only [encPrefixes, Finset.mem_insert, Finset.mem_biUnion, List.mem_toFinset,
+    List.mem_inits] at h
+  rcases h with rfl | ⟨a, ha, hp⟩
+  · simp
+  · have hsup : (encIn a).length + (encOut (f a)).length ≤
+        S.sup fun a => (encIn a).length + (encOut (f a)).length :=
+      Finset.le_sup (f := fun a => (encIn a).length + (encOut (f a)).length) ha
+    have := hp.length_le
+    omega
+
+/-- The machine reaches the state in which it starts emitting the encoded output after a number
+of steps that is bounded independently of the input. -/
+lemma reaches_write (h : ∀ a ∉ S, encOut (f a) = out) (a : α) :
+    ∃ (j : ℕ) (hj : j ≤ (encIn a).length),
+      j + (encOut (f a)).length ≤
+        out.length + S.sup (fun a => (encIn a).length + (encOut (f a)).length) ∧
+      (almostConstTM encIn encOut f S out).runFrom
+          ((almostConstTM encIn encOut f S out).initCfg (encIn a)) (j + 1) =
+        { state := some (Sum.inr ⟨encOut (f a), encOut_mem_outSuffixes h a⟩),
+          inputPos := ⟨1 + j, by omega⟩,
+          workTapes := fun _ _ => none,
+          workTapePos := fun _ => 0,
+          output := [] } := by
+  classical
+  set j := Nat.findGreatest (fun j => (encIn a).take j ∈ encPrefixes encIn S) (encIn a).length
+    with hjdef
+  have hmem : (encIn a).take j ∈ encPrefixes encIn S :=
+    Nat.findGreatest_spec (P := fun j => (encIn a).take j ∈ encPrefixes encIn S)
+      (Nat.zero_le _) (by simp [encPrefixes])
+  have hjle : j ≤ (encIn a).length := Nat.findGreatest_le _
+  have hjsup : j ≤ S.sup fun a => (encIn a).length + (encOut (f a)).length := by
+    have hlen := length_le_sup_of_mem_encPrefixes (encOut := encOut) (f := f) hmem
+    rw [List.length_take] at hlen
+    omega
+  use j, hjle
+  constructor
+  · by_cases ha : a ∈ S
+    · grind [Finset.le_sup (f := fun a => (encIn a).length + (encOut (f a)).length) ha]
+    · grind [h a ha]
+  rw [runFrom_succ_eq_step', runFrom_read a hjle hmem]
+  rcases eq_or_lt_of_le hjle with heq | hlt
+  · -- the whole input has been read, so the machine decodes it
+    have hend : 1 + j = (encIn a).length + 1 := by omega
+    have hdec : encodedFun encIn encOut f S out ((encIn a).take j) = encOut (f a) := by
+      rw [heq, List.take_length]
+      by_cases ha : a ∈ S
+      · exact encodedFun_enc ha
+      · rw [encodedFun_enc_of_notMem ha, h a ha]
+    simp only [step, almostConstTM, Cfg.inputSymbol, Fin.ext_iff, Fin.val_zero, hend,
+      reduceDIte, dite_eq_ite, ite_self, hdec]
+    exact Cfg.ext_zero_tapes rfl (by simp) (by simp)
+  · -- the prefix read so far cannot be extended, so the machine emits the default output
+    have hend : 1 + j ≠ (encIn a).length + 1 := by omega
+    have hprev : 1 + j - 1 = j := by omega
+    have hnotmem : (encIn a).take (j + 1) ∉ encPrefixes encIn S :=
+      Nat.findGreatest_is_greatest (hjdef ▸ Nat.lt_succ_self j) (by omega)
+    have hcat : (encIn a).take j ++ [(encIn a)[j]] ∉ encPrefixes encIn S := by
+      grind [List.take_concat_get']
+    have ha : a ∉ S := fun ha => hnotmem (mem_encPrefixes ha ((encIn a).take_prefix _))
+    have hstart : 1 + j ≠ 0 := by omega
+    simp only [step, almostConstTM, Cfg.inputSymbol, Fin.ext_iff, Fin.val_zero, hstart, hend,
+      hprev, reduceDIte, hcat, moveInputPos_zero]
+    refine Cfg.ext_zero_tapes ?_ (by simp) (by simp)
+    simp only [Option.some.injEq, Sum.inr.injEq, Subtype.mk.injEq]
+    exact (h a ha).symm
+
+/-- The machine `almostConstTM` computes `f` in at most `almostConstTime` steps and no space. -/
+lemma computesFunInTimeAndSpace_almostConstTM (h : ∀ a ∉ S, encOut (f a) = out) :
+    ComputesFunInTimeAndSpace (almostConstTM encIn encOut f S out) encIn encOut f
+      (fun _ => almostConstTime encIn encOut f S out) (fun _ => 0) := by
+  intro a
+  obtain ⟨j, hjle, hj, hrun⟩ := reaches_write h a
+  have hhalt := (almostConstTM encIn encOut f S out).runFrom_add
+    ((almostConstTM encIn encOut f S out).initCfg (encIn a)) (j + 1) ((encOut (f a)).length + 1)
+  rw [hrun, runFrom_write_halted] at hhalt
+  use j + 1 + ((encOut (f a)).length + 1)
+  refine ⟨?_, 0, le_rfl, ?_⟩
+  · change j + 1 + ((encOut (f a)).length + 1) ≤ almostConstTime encIn encOut f S out
+    rw [almostConstTime]
+    omega
+  · unfold ComputesInTimeAndSpace
+    rw [hhalt]
+    simp
+
+end AlmostConstFun
+
+section Results
+
+variable {α β : Type*} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool}
+
+/-- Every function whose encoded output is constant outside of a finite set is computable in time
+`almostConstTime` and zero space. -/
+public theorem computableInTimeAndSpace_almostConstTime
+    (f : α → β) (S : Finset α) (out : List Bool) (h : ∀ a ∉ S, encOut (f a) = out) :
+    ComputableInTimeAndSpace f encIn encOut
+      (fun _ => almostConstTime encIn encOut f S out) (fun _ => 0) :=
+  ⟨0, AlmostConstState encIn encOut f S out, inferInstance, almostConstTM encIn encOut f S out,
+    computesFunInTimeAndSpace_almostConstTM h⟩
+
+/-- Every almost constant function is computable in constant time and zero space. -/
+public theorem computableInTimeAndSpace_of_exists_finite_ne
+    {f : α → β} (h : ∃ b : β, {a : α | f a ≠ b}.Finite) :
+    ∃ c, ComputableInTimeAndSpace f encIn encOut (fun _ => c) (fun _ => 0) := by
+  obtain ⟨b, hb⟩ := h
+  refine ⟨_, computableInTimeAndSpace_almostConstTime f hb.toFinset (encOut b) ?_⟩
+  intro a ha
+  simp only [Set.Finite.mem_toFinset, Set.mem_ofPred_eq, not_not] at ha
+  rw [ha]
+
+/-- Every constant function is computable in constant time and zero space. -/
+public theorem computableInTimeAndSpace_of_const {α β : Type*}
+    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (b : β) :
+    ∃ c, ComputableInTimeAndSpace (Function.const α b) encIn encOut
+      (fun _ => c) (fun _ => 0) :=
+  computableInTimeAndSpace_of_exists_finite_ne ⟨b, by simp⟩
+
+/-- A constant time bound for functions on a finite type. -/
+public noncomputable def finiteFunTime {α β : Type*} [Finite α] (encIn : α ↪ List Bool)
+    (encOut : β ↪ List Bool) (f : α → β) : ℕ :=
+  haveI := Fintype.ofFinite α
+  almostConstTime encIn encOut f Finset.univ []
+
+/-- Every function on a finite type is computable in time `finiteFunTime` and zero space. -/
+public theorem computableInTimeAndSpace_finiteFunTime {α β : Type*} [Finite α]
+    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (f : α → β) :
+    ComputableInTimeAndSpace f encIn encOut
+      (fun _ => finiteFunTime encIn encOut f) (fun _ => 0) :=
+  computableInTimeAndSpace_almostConstTime f (@Finset.univ α (Fintype.ofFinite α)) []
+    fun a ha => absurd (@Finset.mem_univ α (Fintype.ofFinite α) a) ha
+
+/-- Every function on a finite type is computable in constant time and zero space. -/
+public theorem computableInTimeAndSpace_of_finite {α β : Type*} [Finite α]
+    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool}
+    (f : α → β) :
+    ∃ c, ComputableInTimeAndSpace f encIn encOut (fun _ => c) (fun _ => 0) :=
+  ⟨_, computableInTimeAndSpace_finiteFunTime f⟩
+
+end Results
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean
new file mode 100644
index 0000000000..07e468cb6b
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Complexity of composed functions
+
+If `f` and `g` are computable, then so is `g ∘ f`. The machine runs the machine for `f` with its
+output diverted onto a work tape, and then runs the machine for `g` with that tape as its input
+tape.
+
+Note that the intermediate result has to be stored on a work tape: the output tape is append-only
+and cannot be read back. Its length therefore enters both the time and the space bound, and it is
+not bounded by the space used by the machine for `f`, since a machine can produce an output much
+longer than the space it uses.
+
+Recoding the input or the output of a computation is the special case where one of the two
+functions is the identity.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_comp`: the complexity of a composition.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α β γ : Type*}
+
+/-- **Complexity of the identity.** A machine can copy its input to its output one symbol at a
+time, so the identity is computable in linear time and zero space, relative to any encoding.
+
+Together with `computableInTimeAndSpace_comp` this is what recodes a value from one encoding to
+another, and what copies the input of a machine onto a work tape. -/
+public theorem computableInTimeAndSpace_id {enc : α ↪ List Bool} :
+    ∃ c, ComputableInTimeAndSpace (id : α → α) enc enc
+      (fun a => c * ((enc a).length + 1)) (fun _ => 0) :=
+  sorry
+
+/-- **Complexity of a composition.** The bounds are those of the two machines, plus the length of
+the encoded intermediate result, which has to be written to and read from a work tape. -/
+public theorem computableInTimeAndSpace_comp {f : α → β} {g : β → γ}
+    {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
+    {tf sf : α → ℕ} {tg sg : β → ℕ}
+    (hf : ComputableInTimeAndSpace f encA encB tf sf)
+    (hg : ComputableInTimeAndSpace g encB encC tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun a => g (f a)) encA encC
+      (fun a => c * (tf a + tg (f a) + (encB (f a)).length + 1))
+      (fun a => c * (sf a + sg (f a) + (encB (f a)).length + 1)) :=
+  sorry
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean
new file mode 100644
index 0000000000..587369e5db
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean
@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Complexity of a concatenation of two functions
+
+If `f` and `g` are computable, then so is any function whose encoded result is the encoded result
+of `f` followed by the encoded result of `g`. The bounds are the sums of the two bounds, plus one
+rewind of the input tape in time and a constant in space.
+
+The machine runs the machine for `f`, rewinds the input head, and runs the machine for `g` on fresh
+work tapes. The intermediate results are never stored: both machines write straight to the output
+tape, which is append-only, so their outputs end up concatenated. The rewind is what lets the
+second machine read the same input as the first, and it is the reason the input length appears in
+the time bound.
+
+This is the introduction rule of a finite product, dual to the case analysis of
+`Cslib.Computability.Machines.Turing.MultiTape.Combinators.Ite`, which is the elimination rule of a
+finite coproduct. Both are irreducibly machine-level for the same reason: they need the input to be
+presented twice, once to each of the two computations.
+
+Note that only the *syntactic* factorisation of the encoding is required. Producing a pair asks
+nothing of the encoding beyond `henc`, whereas consuming one — reading a component back out —
+is a genuine computability requirement on the encoding, of the kind
+`Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option` collects.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_concat`: the complexity of a concatenation.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_pair`: the special case of a pair.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α β γ δ : Type*}
+
+/-- **Complexity of a concatenation.** If `f` and `g` are computable and the encoded result of `h`
+is the encoded result of `f` followed by the encoded result of `g`, then `h` is computable in the
+sum of the two times plus the length of the input, and in the sum of the two spaces plus a
+constant.
+
+The result is stated for an arbitrary `h` with the assumption that its encoding factors as the
+concatenation, rather than for a fixed pairing, so that it covers whatever the caller happens to be
+encoding — a pair, a tuple, a constructor of an inductive type — and the caller is the one who has
+to know that the concatenation of the two encodings is again injective. -/
+public theorem computableInTimeAndSpace_concat
+    {f : α → β} {g : α → γ} {h : α → δ}
+    {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {encD : δ ↪ List Bool}
+    {tf sf tg sg : α → ℕ}
+    (henc : ∀ x, encD (h x) = encB (f x) ++ encC (g x))
+    (hf : ComputableInTimeAndSpace f encIn encB tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encC tg sg) :
+    ∃ c, ComputableInTimeAndSpace h encIn encD
+      (fun x => tf x + tg x + (encIn x).length + 2)
+      (fun x => sf x + sg x + c) :=
+  sorry
+
+/-- **Complexity of computing a pair.** The special case of `computableInTimeAndSpace_concat` in
+which the two results are packed into a pair, encoded by concatenating the two encodings. It is up
+to the caller to provide such an encoding; this needs the encoding of the first component to
+determine where it ends. -/
+public theorem computableInTimeAndSpace_pair
+    {f : α → β} {g : α → γ}
+    {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
+    {encPair : β × γ ↪ List Bool} {tf sf tg sg : α → ℕ}
+    (henc : ∀ p : β × γ, encPair p = encB p.1 ++ encC p.2)
+    (hf : ComputableInTimeAndSpace f encIn encB tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encC tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun x => (f x, g x)) encIn encPair
+      (fun x => tf x + tg x + (encIn x).length + 2)
+      (fun x => sf x + sg x + c) :=
+  computableInTimeAndSpace_concat (fun x => henc (f x, g x)) hf hg
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Ite.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Ite.lean
new file mode 100644
index 0000000000..cb7c400efc
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Ite.lean
@@ -0,0 +1,213 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Complexity of a case analysis
+
+A case analysis runs a machine that says which case holds and then continues with the machine for
+that case. This file has one primitive, `computableInTimeAndSpace_match`, which does exactly that
+for a scrutinee in an arbitrary finite type; `cond`, `ite` and `dite` are the instances at `Bool`.
+
+## Why the finite case is the primitive and not the binary one
+
+Lean's `ite` is not primitive: `ite c t e` is `Decidable.casesOn`, the recursor of the two
+constructor inductive `Decidable c`, whose constructors carry only proofs. Since `Prop` is erased,
+the computational content of `ite` is exactly the recursor of `Bool`, and a `match` on a finite
+inductive type is that recursor nested once per constructor. So `Bool.rec` is the primitive of the
+*elaborator*.
+
+It is not the right primitive here, because a machine does not nest. Deciding among `n` cases is
+one machine reading a scrutinee of constant length and dispatching from its finite control, which
+is no harder than deciding among two; the nesting is a fiction that the machine never performs.
+Building the finite case analysis out of the binary one therefore does not decompose it into
+anything simpler — it only replays `n - 1` copies of the same argument, and each replay multiplies
+the constants, so the bounds have to be renormalised into a fixed shape at every step to make the
+induction go through. Taking the finite case as the primitive deletes all of that: what remains of
+the arithmetic is three weakenings.
+
+The two are equivalent up to constant factors in both directions, so there is no loss. Tests for
+individual cases, which is what the binary form consumes, and the tag itself, which is what this
+one consumes, are interderivable at constant cost: the tag gives every test by one composition
+with a function on a finite type, and the tests give the tag by running all `n` of them. There is
+consequently no reason to state both.
+
+## Why this has to be a combinator
+
+`cond` is a perfectly ordinary computable *function*: as a map `Bool × β × β → β` it reads a tag
+and streams out the component it selects, in linear time and no space. But that function does not
+give the case analysis, because
+
+```
+fun a => if c a then f a else g a  =  cond ∘ (fun a => (c a, f a, g a))
+```
+
+computes *both* `f a` and `g a`. That costs `tf + tg` instead of `max tf tg`, it stores both
+encoded results on work tapes, and — the real problem — nesting `n` conditionals evaluates `2 ^ n`
+branches instead of `n`. The content of a case analysis is that the branch not taken is never run,
+and that laziness is not expressible by composing total functions: the machine has to choose before
+it runs, which is why this is a combinator with a machine-level branch behind it and not a
+consequence of `computableInTimeAndSpace_comp`.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_match`: the primitive, a case analysis on a
+  scrutinee in a finite type. See `CslibTests.Complexity.Combinators` for worked examples.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_cond`: the recursor of `Bool`.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_ite`: Lean's `ite`, for a decidable predicate.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_dite`: Lean's `dite`, whose branches are defined
+  only under a hypothesis and so are supplied through total extensions.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α β : Type*}
+
+/-- **Complexity of a case analysis on a finite type.** If the scrutinee and every branch are
+computable, then so is the case analysis. The machine runs the machine for `sel`, redirecting its
+output onto a work tape; since the scrutinee's type is finite there are only finitely many possible
+contents, all of constant length, so the finite control can tell them apart in constant time and
+continue with the machine for the branch that is taken, on the original input.
+
+What is asked of the scrutinee's type is not that it be finite but that only finitely many of its
+values be reachable, which is what the machine needs: finitely many possible contents of the work
+tape, of bounded length, for the control to tell apart. For a finite type that is `Set.toFinite _`.
+It is worth the slight extra generality because it admits the selector Lean already generates for
+every inductive type, `ctorIdx`, which lands in `ℕ` and so is barred by a finite-type hypothesis.
+Branches outside the range are for the same reason not asked to be computable — with an `ℕ`-indexed
+family, all but finitely many of them are junk.
+
+A single pair of bounds covers the scrutinee and every branch. Nothing is lost by that: given
+separate bounds, weakening each of them to their supremum and applying this gives back exactly the
+statement with the supremum in it, so the two forms are interderivable. The number of cases is a
+constant of the type and is absorbed into the constant factor, as is the cost of rewinding the
+input, which is bounded by the time already spent.
+
+For the same reason a supremum over the branches would not have expressed that only the branch
+taken is executed: the index type is finite with a cardinality fixed by the type, so a supremum and
+a sum over it differ by a constant factor and an implementation running *every* branch would meet
+either bound. What does express it is that no time bound appears in the space bound. A machine
+computing all the branches has to park their encoded outputs on work tapes, and an output's length
+is bounded only by the time that produced it, so its space would be `s a + t a`.
+
+A branch only has to *agree* with the function being computed where it is taken; what it does
+elsewhere is irrelevant, since it is never run there. That is what `hagree` says. It is what a
+`match` that destructures data needs — the machine extracting a constructor's payload is only
+meaningful on encodings of that constructor, so the branch built from it has to be extended by junk
+to become a total function, and the junk must not have to be accounted for — and it is what `dite`
+needs, where a branch is not even defined outside its case. The same weakening lets a computable
+function be patched at finitely many points, by taking the scrutinee to be membership in the finite
+set of exceptions.
+
+`f` carries no information — it is `fun a => br (sel a) a` up to `funext`, and stating the
+conclusion for that function directly would do just as well. It is kept because it is what a
+caller has: their goal is a `match`, not an application of the branch family, and putting the
+conversion in this hypothesis saves them from doing it themselves with `ComputableInTimeAndSpace`
+`.congr` at every use. It is inferred from the goal, so apply this with `exact` or `refine` rather
+than with `obtain`; with no expected type there is nothing to infer `f` from and `hagree` will fix
+it to the wrong function.
+
+This is a case analysis, not a recursor: a `match` on a *recursive* inductive type is a fold, whose
+combinator is the loop of `Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop` with an
+iteration bound.
+
+The branches may perfectly well have different result types: take the output type to be `Σ i, β i`
+and the branches to be `fun i a => ⟨i, br i a⟩`. Making the statement dependent would gain nothing,
+because computability depends only on the two encoded strings and not on the types they encode —
+that is `ComputableInTimeAndSpace.congr` — so a `motive` has no computational content. The
+genuinely dependent conclusion, about a function `(a : α) → β (sel a)`, cannot even be stated: it
+has no single output encoding. The tag that the sigma carries is not overhead either, since without
+it the result would in general not be decodable. -/
+public theorem computableInTimeAndSpace_match {ι : Type}
+    {sel : α → ι} {f : α → β} {br : ι → α → β}
+    {encIn : α ↪ List Bool} {encι : ι ↪ List Bool} {encOut : β ↪ List Bool}
+    {t s : α → ℕ}
+    (hfin : (Set.range sel).Finite)
+    (hagree : ∀ a, br (sel a) a = f a)
+    (hsel : ComputableInTimeAndSpace sel encIn encι t s)
+    (hbr : ∀ i ∈ Set.range sel, ComputableInTimeAndSpace (br i) encIn encOut t s) :
+    ∃ c, ComputableInTimeAndSpace f encIn encOut
+      (fun a => c * (t a + 1)) (fun a => c * (s a + 1)) :=
+  sorry
+
+/-- **Complexity of a two-way case analysis**, the recursor of `Bool`. This is
+`computableInTimeAndSpace_match` at `ι = Bool`, with the common bound taken to be the test plus the
+larger of the two branches. -/
+public theorem computableInTimeAndSpace_cond {sel : α → Bool} {_if _else : α → β}
+    {encIn : α ↪ List Bool} {encCond : Bool ↪ List Bool} {encOut : β ↪ List Bool}
+    {tc sc tif sif telse selse : α → ℕ}
+    (hsel : ComputableInTimeAndSpace sel encIn encCond tc sc)
+    (hif : ComputableInTimeAndSpace _if encIn encOut tif sif)
+    (helse : ComputableInTimeAndSpace _else encIn encOut telse selse) :
+    ∃ c, ComputableInTimeAndSpace (fun a => if sel a then _if a else _else a) encIn encOut
+      (fun a => c * (tc a + max (tif a) (telse a) + 1))
+      (fun a => c * (sc a + max (sif a) (selse a) + 1)) := by
+  refine computableInTimeAndSpace_match (encι := encCond)
+    (br := fun b a => bif b then _if a else _else a) (Set.toFinite _)
+    (fun a => by cases sel a <;> simp)
+    (hsel.mono (fun a => Nat.le_add_right _ _) (fun a => Nat.le_add_right _ _))
+    (fun b _ => by
+      cases b
+      · exact helse.mono (fun a => by have := le_max_right (tif a) (telse a); omega)
+          (fun a => by have := le_max_right (sif a) (selse a); omega)
+      · exact hif.mono (fun a => by have := le_max_left (tif a) (telse a); omega)
+          (fun a => by have := le_max_left (sif a) (selse a); omega))
+
+/-- **Complexity of Lean's `ite`.** A conditional on a decidable predicate, given a machine that
+decides it. This is `computableInTimeAndSpace_cond` read through `decide`: the `Decidable` instance
+of `ite` carries no computational content, so all that is needed of the predicate is that its
+Boolean test is computable — which for a language is exactly `DecidableInTimeAndSpace`. -/
+public theorem computableInTimeAndSpace_ite {p : α → Prop} [DecidablePred p] {_if _else : α → β}
+    {encIn : α ↪ List Bool} {encCond : Bool ↪ List Bool} {encOut : β ↪ List Bool}
+    {tc sc tif sif telse selse : α → ℕ}
+    (hp : ComputableInTimeAndSpace (fun a => decide (p a)) encIn encCond tc sc)
+    (hif : ComputableInTimeAndSpace _if encIn encOut tif sif)
+    (helse : ComputableInTimeAndSpace _else encIn encOut telse selse) :
+    ∃ c, ComputableInTimeAndSpace (fun a => if p a then _if a else _else a) encIn encOut
+      (fun a => c * (tc a + max (tif a) (telse a) + 1))
+      (fun a => c * (sc a + max (sif a) (selse a) + 1)) := by
+  obtain ⟨c, hc⟩ := computableInTimeAndSpace_cond hp hif helse
+  refine ⟨c, ?_⟩
+  have hfun : (fun a => if decide (p a) = true then _if a else _else a) =
+      fun a => if p a then _if a else _else a := by
+    funext a
+    simp
+  rwa [hfun] at hc
+
+/-- **Complexity of Lean's `dite`.** The branches of a `dite` are not functions of the input alone:
+each is defined only under the hypothesis that its case holds, so neither can be asked to be
+computable as it stands. What is asked instead is a computable *total* function agreeing with the
+branch where that branch is taken, which is `computableInTimeAndSpace_match`'s `hagree` in the
+concrete case `ι = Bool`. Outside its case a branch may be anything at all, which is exactly the
+freedom needed to extend it to a total function. -/
+public theorem computableInTimeAndSpace_dite {p : α → Prop} [DecidablePred p]
+    {_if : (a : α) → p a → β} {_else : (a : α) → ¬ p a → β} {If Else : α → β}
+    {encIn : α ↪ List Bool} {encCond : Bool ↪ List Bool} {encOut : β ↪ List Bool}
+    {tc sc tif sif telse selse : α → ℕ}
+    (hIf : ∀ a (h : p a), If a = _if a h)
+    (hElse : ∀ a (h : ¬ p a), Else a = _else a h)
+    (hp : ComputableInTimeAndSpace (fun a => decide (p a)) encIn encCond tc sc)
+    (hif : ComputableInTimeAndSpace If encIn encOut tif sif)
+    (helse : ComputableInTimeAndSpace Else encIn encOut telse selse) :
+    ∃ c, ComputableInTimeAndSpace (fun a => dite (p a) (_if a) (_else a)) encIn encOut
+      (fun a => c * (tc a + max (tif a) (telse a) + 1))
+      (fun a => c * (sc a + max (sif a) (selse a) + 1)) := by
+  obtain ⟨c, hc⟩ := computableInTimeAndSpace_ite (p := p) hp hif helse
+  refine ⟨c, ?_⟩
+  have hfun : (fun a => if p a then If a else Else a) =
+      fun a => dite (p a) (_if a) (_else a) := by
+    funext a
+    by_cases h : p a
+    · simp [h, hIf a h]
+    · simp [h, hElse a h]
+  rwa [hfun] at hc
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Loop.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Loop.lean
new file mode 100644
index 0000000000..9c1ff1f366
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Loop.lean
@@ -0,0 +1,800 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Basic.Finite.Sum
+public import Mathlib.Data.PFun
+public import Mathlib.Tactic.Ring
+public import Mathlib.Computability.StateTransition
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp
+public import Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Words
+
+/-!
+# Loop combinator
+
+This file is about the loop whose condition and body are fused into a single function
+`body : α → Option α`, which returns `none` exactly when the loop is to stop:
+
+```
+loop
+  match body a with
+  | none => return a
+  | some a' => a := a'
+```
+
+This is the form in which the loop is implemented by a machine, since it needs only one machine for
+the whole loop body. The usual `while` loop, with a separate condition and body, is derived from it
+in `Cslib.Computability.Machines.Turing.MultiTape.Combinators.While`.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.loopFunction`: the partial function computed by the loop, defined as
+  `StateTransition.eval` of the loop body. It is undefined on the inputs for which the loop
+  diverges.
+* `Turing.MultiTapeTM.loopIterate`: the value after a given number of iterations, or `none` if the
+  loop has already stopped.
+
+## Main results
+
+* `Turing.MultiTapeTM.mem_loopFunction_iff`: the loop started at `a` terminates in `b` exactly if
+  `b` is an iterate of `a` at which the body stops.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_loopFunction`: the complexity of the loop.
+-/
+
+namespace Turing.MultiTapeTM
+
+variable {α : Type*}
+
+/-- The partial function computed by the loop with the fused body `body`, which returns `none`
+exactly when the loop is to stop. It is defined exactly on the inputs for which the loop
+terminates. -/
+@[expose] public def loopFunction (body : α → Option α) : α →. α := StateTransition.eval body
+
+/-- The value after `n` iterations of the fused loop body, or `none` if the loop has stopped
+after at most `n` iterations. -/
+@[expose] public def loopIterate (body : α → Option α) : ℕ → α → Option α
+  | 0, a => some a
+  | n + 1, a => (body a).bind (loopIterate body n)
+
+section Iterate
+
+/-! ## The iterates of the loop body
+
+The loop is described by two views of its body: `loopIterate`, which is what the machine actually
+runs through, and `loopFunction`, which is what it computes. This section relates them.
+-/
+
+variable {body : α → Option α}
+
+@[simp]
+public lemma loopIterate_zero (a : α) : loopIterate body 0 a = some a := rfl
+
+public lemma loopIterate_succ (n : ℕ) (a : α) :
+    loopIterate body (n + 1) a = (body a).bind (loopIterate body n) := rfl
+
+@[simp]
+public lemma loopIterate_one (a : α) : loopIterate body 1 a = body a := by
+  cases h : body a <;> simp [loopIterate_succ, h]
+
+/-- The iterates of the loop body compose. -/
+public lemma loopIterate_add (m n : ℕ) (a : α) :
+    loopIterate body (m + n) a = (loopIterate body m a).bind (loopIterate body n) := by
+  induction m generalizing a with
+  | zero => simp
+  | succ m ih =>
+    cases h : body a with
+    | none => simp [show m + 1 + n = m + n + 1 by omega, loopIterate_succ, h]
+    | some b => simp [show m + 1 + n = m + n + 1 by omega, loopIterate_succ, h, ih]
+
+/-- One more iteration can also be performed at the end. -/
+public lemma loopIterate_succ' (n : ℕ) (a : α) :
+    loopIterate body (n + 1) a = (loopIterate body n a).bind body := by
+  rw [loopIterate_add]
+  simp
+
+/-- Once the loop has stopped it stays stopped. -/
+public lemma loopIterate_eq_none_of_le {m n : ℕ} {a : α} (h : m ≤ n)
+    (hm : loopIterate body m a = none) : loopIterate body n a = none := by
+  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h
+  rw [loopIterate_add, hm]
+  rfl
+
+/-- Before the loop has stopped it has not stopped. -/
+public lemma loopIterate_ne_none_of_le {m n : ℕ} {a : α} (h : m ≤ n)
+    (hn : loopIterate body n a ≠ none) : loopIterate body m a ≠ none :=
+  fun hm => hn (loopIterate_eq_none_of_le h hm)
+
+/-- As long as the loop has not stopped, each iterate is obtained from the previous one by a
+successful call of the body. -/
+public lemma loopIterate_succ_of_lt {m n : ℕ} {a x : α} (hn : n < m)
+    (hm : loopIterate body m a ≠ none) (hx : loopIterate body n a = some x) :
+    ∃ x', body x = some x' ∧ loopIterate body (n + 1) a = some x' := by
+  have heq : loopIterate body (n + 1) a = body x := by rw [loopIterate_succ', hx]; simp
+  have hne : body x ≠ none := heq ▸ loopIterate_ne_none_of_le hn hm
+  obtain ⟨x', hx'⟩ := Option.ne_none_iff_exists'.mp hne
+  exact ⟨x', hx', by rw [heq, hx']⟩
+
+/-- The values reachable by repeatedly applying the loop body are exactly its iterates. -/
+public lemma reaches_iff_loopIterate {a b : α} :
+    Relation.ReflTransGen (fun x y => y ∈ body x) a b ↔ ∃ n, loopIterate body n a = some b := by
+  constructor
+  · intro h
+    induction h using Relation.ReflTransGen.head_induction_on with
+    | refl => exact ⟨0, rfl⟩
+    | head hstep _ ih =>
+      obtain ⟨n, hn⟩ := ih
+      exact ⟨n + 1, by rw [loopIterate_succ, Option.mem_def.mp hstep]; exact hn⟩
+  · rintro ⟨n, hn⟩
+    induction n generalizing a with
+    | zero =>
+      rw [loopIterate_zero, Option.some_inj] at hn
+      exact hn ▸ Relation.ReflTransGen.refl
+    | succ n ih =>
+      rw [loopIterate_succ] at hn
+      cases hc : body a with
+      | none => rw [hc] at hn; simp at hn
+      | some c =>
+        rw [hc] at hn
+        exact Relation.ReflTransGen.head (Option.mem_def.mpr hc) (ih hn)
+
+/-- **The graph of `loopFunction`.** The loop started at `a` terminates in `b` exactly if `b` is an
+iterate of `a` at which the body stops. -/
+public theorem mem_loopFunction_iff {a b : α} :
+    b ∈ loopFunction body a ↔ ∃ n, loopIterate body n a = some b ∧ body b = none := by
+  rw [loopFunction, StateTransition.mem_eval, StateTransition.Reaches, reaches_iff_loopIterate]
+  exact ⟨fun ⟨⟨n, hn⟩, hb⟩ => ⟨n, hn, hb⟩, fun ⟨n, hn, hb⟩ => ⟨⟨n, hn⟩, hb⟩⟩
+
+end Iterate
+
+section Bounds
+
+/-! ## Arithmetic helpers
+
+Every machine that the loop is assembled from costs a constant times the sum of a few lengths, and
+every one of those lengths is bounded by a constant times `s a + 1` or `t a + s a + 1`. These
+lemmas turn such a sum into a single constant times the bound. -/
+
+private lemma nat_bound₀ {W u X : ℕ} (hu : 1 ≤ u) (hX : X ≤ W * u) : X + 1 ≤ (W + 1) * u := by
+  calc X + 1 ≤ W * u + u := Nat.add_le_add hX hu
+    _ = (W + 1) * u := by ring
+
+private lemma nat_bound₁ {c W u X : ℕ} (hu : 1 ≤ u) (hX : X ≤ W * u) :
+    c * (X + 1) ≤ c * (W + 1) * u := by
+  calc c * (X + 1) ≤ c * (W * u + u) := by gcongr
+    _ = c * (W + 1) * u := by ring
+
+private lemma nat_bound₂ {c W u X Y : ℕ} (hu : 1 ≤ u) (hX : X ≤ W * u) (hY : Y ≤ W * u) :
+    c * (X + Y + 1) ≤ c * (2 * W + 1) * u := by
+  calc c * (X + Y + 1) ≤ c * (W * u + W * u + u) := by gcongr
+    _ = c * (2 * W + 1) * u := by ring
+
+private lemma nat_bound₃ {c W u X Y Z : ℕ} (hu : 1 ≤ u) (hX : X ≤ W * u) (hY : Y ≤ W * u)
+    (hZ : Z ≤ W * u) : c * (X + Y + Z + 1) ≤ c * (3 * W + 1) * u := by
+  calc c * (X + Y + Z + 1) ≤ c * (W * u + W * u + W * u + u) := by gcongr
+    _ = c * (3 * W + 1) * u := by ring
+
+/-- A constant summand is absorbed into the constant factor. -/
+private lemma nat_bound_add {c d u X : ℕ} (hu : 1 ≤ u) (hX : X ≤ c * u) : X + d ≤ (c + d) * u := by
+  calc X + d ≤ c * u + d * u := by gcongr; exact Nat.le_mul_of_pos_right d (by omega)
+    _ = (c + d) * u := by ring
+
+end Bounds
+
+section TapeWords
+
+/-! ## The vector of words on three named tapes
+
+Every configuration the loop machine passes through is blank outside of three named work tapes;
+`tapeWords` is the vector of words of such a configuration. The machines of
+`Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Words` return whole vectors — their
+postconditions are equalities — so the projection, blankness and `Function.update` equations here
+are all that is needed to glue the steps of the loop. -/
+
+variable {K : ℕ}
+
+/-- The vector of words that holds `w₁`, `w₂` and `w₃` on the tapes `i₁`, `i₂` and `i₃` and is
+blank everywhere else. -/
+private def tapeWords (i₁ i₂ i₃ : Fin K) (w₁ w₂ w₃ : List Bool) : Fin K → List Bool :=
+  fun l => if l = i₁ then w₁ else if l = i₂ then w₂ else if l = i₃ then w₃ else []
+
+variable {i₁ i₂ i₃ : Fin K} {w₁ w₂ w₃ w : List Bool}
+
+private lemma tapeWords_fst : tapeWords i₁ i₂ i₃ w₁ w₂ w₃ i₁ = w₁ := by
+  simp [tapeWords]
+
+private lemma tapeWords_snd (h₁₂ : i₁ ≠ i₂) : tapeWords i₁ i₂ i₃ w₁ w₂ w₃ i₂ = w₂ := by
+  simp [tapeWords, Ne.symm h₁₂]
+
+private lemma tapeWords_thd (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
+    tapeWords i₁ i₂ i₃ w₁ w₂ w₃ i₃ = w₃ := by
+  simp [tapeWords, Ne.symm h₁₃, Ne.symm h₂₃]
+
+private lemma tapeWords_of_ne_fst {l : Fin K} (h₁ : l ≠ i₁) :
+    tapeWords i₁ i₂ i₃ w₁ [] [] l = [] := by
+  simp [tapeWords, h₁]
+
+private lemma tapeWords_of_ne_snd {l : Fin K} (h₂ : l ≠ i₂) :
+    tapeWords i₁ i₂ i₃ [] w₂ [] l = [] := by
+  simp [tapeWords, h₂]
+
+private lemma tapeWords_of_ne_fst_snd {l : Fin K} (h₁ : l ≠ i₁) (h₂ : l ≠ i₂) :
+    tapeWords i₁ i₂ i₃ w₁ w₂ [] l = [] := by
+  simp [tapeWords, h₁, h₂]
+
+private lemma update_tapeWords_fst :
+    Function.update (tapeWords i₁ i₂ i₃ w₁ w₂ w₃) i₁ w = tapeWords i₁ i₂ i₃ w w₂ w₃ := by
+  funext l
+  by_cases h : l = i₁
+  · subst h; rw [Function.update_self, tapeWords_fst]
+  · rw [Function.update_of_ne h]; simp [tapeWords, h]
+
+private lemma update_tapeWords_snd (h₁₂ : i₁ ≠ i₂) :
+    Function.update (tapeWords i₁ i₂ i₃ w₁ w₂ w₃) i₂ w = tapeWords i₁ i₂ i₃ w₁ w w₃ := by
+  funext l
+  by_cases h : l = i₂
+  · subst h; rw [Function.update_self, tapeWords_snd h₁₂]
+  · rw [Function.update_of_ne h]; simp [tapeWords, h]
+
+private lemma update_tapeWords_thd (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
+    Function.update (tapeWords i₁ i₂ i₃ w₁ w₂ w₃) i₃ w = tapeWords i₁ i₂ i₃ w₁ w₂ w := by
+  funext l
+  by_cases h : l = i₃
+  · subst h; rw [Function.update_self, tapeWords_thd h₁₃ h₂₃]
+  · rw [Function.update_of_ne h]; simp [tapeWords, h]
+
+end TapeWords
+
+-- The `Finite` instances of the machines that are combined are produced by `obtain`, so they have
+-- to be registered as instances with `haveI` even though the goal is a proposition.
+set_option linter.style.haveILetI false in
+/-- **Complexity of a loop.**
+
+Assume that
+* `f` picks, for every input, a value at which the loop terminates (`hf`), and the loop started at
+  `a` stops after at most `iterBound a` iterations (`hiter`);
+* the loop body is computable in time `t` and space `s` (`hbody`), where `s` also bounds the
+  encoded length of all the values encountered while running the loop (`hsize`, which includes `a`
+  itself);
+* these bounds do not increase along the iterations of the loop (`ht`, `hs`).
+
+Then `f` is computable in time proportional to the number of iterations times the cost of one
+iteration, and in space proportional to the space of one iteration.
+
+The machine uses three named work tapes, `T1` holding the current value, `T3` holding the result of
+the last call of the body and `T4` holding the flag that says whether the loop is over, plus the
+scratch tapes of the machines it runs, which `exists_transformsTapes_ofComputable` hides. It first
+copies its input onto `T1` and runs the machine for `body` with `T1` as its input tape and `T3` as
+its output tape. Then it repeats: run the machine for `Option.isNone` on `T3`, writing the flag to
+`T4`, and branch on the flag; if the loop is over, stop, so that the contents of `T1` can be
+emitted; otherwise clear `T4`, clear `T1`, run the destructor of `some` with `T3` as its input and
+`T1` as its output, clear `T3` and run the body again with `T1` as its input and `T3` as its
+output.
+
+Note that `T1` has to be kept until the result of the body has been inspected, since on exit the
+result of the loop is the value that was fed to the last call of the body. Copying the input onto
+`T1` before the first call of the body costs only `O(s a)`, since `hsize` bounds the length of the
+encoded input.
+
+The space bound of the body alone does not bound the encoded length of the intermediate values: the
+input tape is read-only and the output tape is append-only, so neither counts towards the space
+bound, and a machine can produce an output much longer than the space it uses. The intermediate
+values, however, are stored on a work tape, and hence `hsize` is a genuine additional assumption on
+`s`. Since the resulting bounds are stated up to a constant factor, using a single `s` for both
+purposes is no weaker than using two separate bounds, whose maximum `s` can be taken to be. -/
+public theorem computableInTimeAndSpace_loopFunction
+    {α : Type*} {body : α → Option α} {f : α → α}
+    {enc : α ↪ List Bool} {encOpt : Option α ↪ List Bool} {t s iterBound : α → ℕ}
+    (henc : IsOptionEncoding enc encOpt)
+    (hf : ∀ a, f a ∈ loopFunction body a)
+    (hiter : ∀ a, ∃ m ≤ iterBound a, loopIterate body m a = none)
+    (hsize : ∀ a m x, loopIterate body m a = some x → (enc x).length ≤ s a)
+    (hbody : ComputableInTimeAndSpace body enc encOpt t s)
+    (ht : ∀ a m x, loopIterate body m a = some x → t x ≤ t a)
+    (hs : ∀ a m x, loopIterate body m a = some x → s x ≤ s a) :
+    ∃ c, ComputableInTimeAndSpace f enc enc
+      (fun a => c * (iterBound a + 1) * (t a + s a + 1))
+      (fun a => c * (s a + 1)) := by
+  classical
+  -- ### The number of iterations
+  -- `N a` is the number of iterations after which the loop started at `a` stops, and `f a` is the
+  -- value it stops at.
+  have hkey : ∀ a, ∃ n, loopIterate body n a = some (f a) ∧ body (f a) = none :=
+    fun a => mem_loopFunction_iff.mp (hf a)
+  choose N hN hNstop using hkey
+  have hNle : ∀ a, N a + 1 ≤ iterBound a := by
+    intro a
+    obtain ⟨m, hm, hmnone⟩ := hiter a
+    have hlt : N a < m := by
+      by_contra hcon
+      have hcontra := loopIterate_eq_none_of_le (Nat.le_of_not_lt hcon) hmnone
+      rw [hN a] at hcontra
+      simp at hcontra
+    omega
+  -- every round before `N a` produces the value the next one starts at
+  have hnext : ∀ a n, n < N a → ∀ x, loopIterate body n a = some x →
+      ∃ x', body x = some x' ∧ loopIterate body (n + 1) a = some x' :=
+    fun a n hn x hx => loopIterate_succ_of_lt hn
+      (by rw [hN a]; exact Option.some_ne_none _) hx
+  -- ### The encoding of the loop flag
+  obtain ⟨encBool, hencBoolHead, hencBoolLen⟩ :
+      ∃ e : Bool ↪ List Bool, (∀ b, (e b).head? = some b) ∧ ∀ b, (e b).length = 1 :=
+    ⟨⟨fun b => [b], fun b₁ b₂ h => by simpa using h⟩, fun _ => rfl, fun _ => rfl⟩
+  -- ### Lengths of the encodings encountered along the loop
+  obtain ⟨cc, hcc⟩ := henc.constructor_computable
+  have hccLen : ∀ x : α, (encOpt (some x)).length ≤ cc * ((enc x).length + 1) :=
+    hcc.length_encOut_le
+  obtain ⟨E, hE⟩ : ∃ E, ∀ a n x, loopIterate body n a = some x →
+      (encOpt (body x)).length ≤ E * (s a + 1) := by
+    refine ⟨cc + (encOpt none).length, fun a n x hx => ?_⟩
+    rcases hb : body x with _ | x'
+    · calc (encOpt none).length ≤ cc + (encOpt none).length := Nat.le_add_left _ _
+        _ ≤ (cc + (encOpt none).length) * (s a + 1) :=
+            Nat.le_mul_of_pos_right _ (Nat.succ_pos _)
+    · have hx' : loopIterate body (n + 1) a = some x' := by
+        rw [loopIterate_succ', hx]; simpa using hb
+      calc (encOpt (some x')).length ≤ cc * ((enc x').length + 1) := hccLen x'
+        _ ≤ cc * (s a + 1) := Nat.mul_le_mul_left _ (by have := hsize a (n + 1) x' hx'; omega)
+        _ ≤ (cc + (encOpt none).length) * (s a + 1) := Nat.mul_le_mul_right _ (by omega)
+  -- ### The machines the loop is assembled from
+  obtain ⟨cd, hd⟩ := henc.destructor_computable
+  obtain ⟨cn, hisNone⟩ :=
+    computableInTimeAndSpace_isNone (α := α) (encOpt := encOpt) (encBool := encBool)
+  obtain ⟨ci, hid⟩ := computableInTimeAndSpace_id (α := α) (enc := enc)
+  obtain ⟨mB, cB, hB⟩ := exists_transformsTapes_ofComputable hbody
+  obtain ⟨mD, cD, hD⟩ := exists_transformsTapes_ofComputable hd
+  obtain ⟨mN, cN, hNm⟩ := exists_transformsTapes_ofComputable hisNone
+  obtain ⟨mI, cI, hI⟩ := exists_transformsTapes_ofComputableInput hid
+  -- the tape layout: `T1` the current value, `T3` the result of the body, `T4` the flag
+  obtain ⟨K, T1, T3, T4, hT13, hT14, hT34, hKB, hKD, hKN, hKI⟩ :
+      ∃ (K : ℕ) (T1 T3 T4 : Fin K), T1 ≠ T3 ∧ T1 ≠ T4 ∧ T3 ≠ T4 ∧
+        mB + 2 ≤ K ∧ mD + 2 ≤ K ∧ mN + 3 ≤ K ∧ mI + 1 ≤ K :=
+    ⟨mB + mD + mN + mI + 5, ⟨0, by omega⟩, ⟨1, by omega⟩, ⟨2, by omega⟩,
+      Fin.ne_of_val_ne (by simp), Fin.ne_of_val_ne (by simp), Fin.ne_of_val_ne (by simp),
+      by omega, by omega, by omega, by omega⟩
+  obtain ⟨SB, hSB, MBody, hMBody⟩ :=
+    hB K T1 T3 ∅ hT13 (by simp) (by simp) (by simpa using hKB)
+  obtain ⟨SD, hSD, MDestr, hMDestr⟩ :=
+    hD K T3 T1 ∅ (Ne.symm hT13) (by simp) (by simp) (by simpa using hKD)
+  obtain ⟨SN, hSN, MIsNone, hMIsNone⟩ :=
+    hNm K T3 T4 {T1} hT34 (by simpa using Ne.symm hT13) (by simpa using Ne.symm hT14)
+      (by simp only [Finset.card_singleton]; omega)
+  obtain ⟨SI, hSI, MCopy, hMCopy⟩ := hI K T1 ∅ (by simp) (by simpa using hKI)
+  obtain ⟨cC1, SC1, hSC1, MClear1, hMClear1⟩ := exists_transformsTapes_clear T1
+  obtain ⟨cC3, SC3, hSC3, MClear3, hMClear3⟩ := exists_transformsTapes_clear T3
+  obtain ⟨cC4, SC4, hSC4, MClear4, hMClear4⟩ := exists_transformsTapes_clear T4
+  obtain ⟨SNop, hSNop, MNop, hMNop⟩ := exists_transformsTapes_nop K
+  haveI := hSB; haveI := hSD; haveI := hSN; haveI := hSI
+  haveI := hSC1; haveI := hSC3; haveI := hSC4; haveI := hSNop
+  -- ### One constant bounding every length that occurs
+  obtain ⟨W, hW1, hWcn, hWci, hWlen⟩ : ∃ W : ℕ, 1 ≤ W ∧ cn ≤ W ∧ ci ≤ W ∧
+      ∀ a n x, loopIterate body n a = some x →
+        (enc x).length ≤ W * (s a + 1) ∧
+        (encOpt (body x)).length ≤ W * (s a + 1) ∧
+        (encOpt (some x)).length ≤ W * (s a + 1) ∧
+        cd * ((encOpt (some x)).length + 1) ≤ W * (s a + 1) ∧
+        s x ≤ W * (s a + 1) ∧ t x ≤ W * (t a + s a + 1) := by
+    refine ⟨cn + ci + cc + E + cd * (cc + 1) + 1, by omega, by omega, by omega,
+      fun a n x hx => ⟨?_, ?_, ?_, ?_, ?_, ?_⟩⟩
+    · exact le_trans (by have := hsize a n x hx; omega)
+        (Nat.le_mul_of_pos_left _ (by omega))
+    · exact (hE a n x hx).trans (Nat.mul_le_mul_right _ (by omega))
+    · exact (hccLen x).trans ((Nat.mul_le_mul_left _ (by have := hsize a n x hx; omega)).trans
+        (Nat.mul_le_mul_right _ (by omega)))
+    · have h1 : (encOpt (some x)).length ≤ cc * (s a + 1) :=
+        (hccLen x).trans (Nat.mul_le_mul_left _ (by have := hsize a n x hx; omega))
+      calc cd * ((encOpt (some x)).length + 1)
+          ≤ cd * (cc * (s a + 1) + (s a + 1)) :=
+            Nat.mul_le_mul_left _ (Nat.add_le_add h1 (by omega))
+        _ = cd * (cc + 1) * (s a + 1) := by ring
+        _ ≤ _ := Nat.mul_le_mul_right _ (by omega)
+    · exact le_trans (by have := hs a n x hx; omega) (Nat.le_mul_of_pos_left _ (by omega))
+    · exact le_trans (by have := ht a n x hx; omega) (Nat.le_mul_of_pos_left _ (by omega))
+  -- the two units in which the bounds are measured
+  have hu1 : ∀ a, 1 ≤ t a + s a + 1 := fun a => by omega
+  have hv1 : ∀ a, 1 ≤ s a + 1 := fun a => by omega
+  have hvu : ∀ (a : α) (c : ℕ), c * (s a + 1) ≤ c * (t a + s a + 1) :=
+    fun a c => Nat.mul_le_mul_left _ (by omega)
+  -- ### Descriptions of the tape contents at the various points of a round
+  -- Every configuration of the loop is a `tapeWords T1 T3 T4` vector, and the machines return
+  -- whole vectors, so the steps below are glued by rewriting with the equations of `tapeWords`.
+  -- The predicates are obtained from existentials so that they are unfolded only where intended.
+  obtain ⟨Pround, hPround⟩ : ∃ P : α → ℕ → (Fin K → List Bool) → Prop, ∀ a n ws, P a n ws ↔
+      (∃ y, loopIterate body n a = some y ∧
+        ws = tapeWords T1 T3 T4 (enc y) (encOpt (body y)) []) := ⟨_, fun _ _ _ => Iff.rfl⟩
+  obtain ⟨PMid, hPMid⟩ : ∃ P : α → ℕ → (Fin K → List Bool) → Prop, ∀ a n ws, P a n ws ↔
+      (∃ y, loopIterate body n a = some y ∧
+        ws = tapeWords T1 T3 T4 (enc y) (encOpt (body y)) (encBool (body y).isNone)) :=
+    ⟨_, fun _ _ _ => Iff.rfl⟩
+  obtain ⟨PExit, hPExit⟩ : ∃ P : α → ℕ → (Fin K → List Bool) → Prop, ∀ a n ws, P a n ws ↔
+      (∃ y, loopIterate body n a = some y ∧ body y = none ∧
+        ws = tapeWords T1 T3 T4 (enc y) (encOpt (body y)) (encBool (body y).isNone)) :=
+    ⟨_, fun _ _ _ => Iff.rfl⟩
+  obtain ⟨PCont, hPCont⟩ : ∃ P : α → ℕ → (Fin K → List Bool) → Prop, ∀ a n ws, P a n ws ↔
+      (∃ y y', loopIterate body n a = some y ∧ body y = some y' ∧
+        ws = tapeWords T1 T3 T4 (enc y) (encOpt (body y)) (encBool (body y).isNone)) :=
+    ⟨_, fun _ _ _ => Iff.rfl⟩
+  obtain ⟨QR, hQR⟩ : ∃ Q : α → ℕ → (Fin K → List Bool) → Prop, ∀ a n ws', Q a n ws' ↔
+      ((∀ y, loopIterate body n a = some y → body y = none →
+          ws' T1 = enc y ∧ (ws' T4).head? = some true) ∧
+       (∀ y y', loopIterate body n a = some y → body y = some y' →
+          ws' = tapeWords T1 T3 T4 (enc y') (encOpt (body y')) [] ∧
+            (ws' T4).head? ≠ some true)) :=
+    ⟨_, fun _ _ _ => Iff.rfl⟩
+  -- ### Bounds for the individual machines
+  -- Every length occurring in the bound of a machine of a round is bounded by `W * (s a + 1)`,
+  -- hence its time by a constant times `t a + s a + 1` and its space by a constant times `s a + 1`.
+  have hWt : ∀ a n x, loopIterate body n a = some x →
+      (enc x).length ≤ W * (t a + s a + 1) ∧
+      (encOpt (body x)).length ≤ W * (t a + s a + 1) ∧
+      (encOpt (some x)).length ≤ W * (t a + s a + 1) ∧
+      cd * ((encOpt (some x)).length + 1) ≤ W * (t a + s a + 1) ∧
+      s x ≤ W * (t a + s a + 1) ∧ t x ≤ W * (t a + s a + 1) := by
+    intro a n x hx
+    obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hWlen a n x hx
+    exact ⟨h1.trans (hvu a W), h2.trans (hvu a W), h3.trans (hvu a W), h4.trans (hvu a W),
+      h5.trans (hvu a W), h6⟩
+  have hcW : ∀ (c : ℕ) (a : α), c ≤ W → c ≤ W * (t a + s a + 1) := fun c a hc =>
+    hc.trans (Nat.le_mul_of_pos_right _ (by omega))
+  have hcWv : ∀ (c : ℕ) (a : α), c ≤ W → c ≤ W * (s a + 1) := fun c a hc =>
+    hc.trans (Nat.le_mul_of_pos_right _ (by omega))
+  obtain ⟨A1, hA1⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cN * (cn + (encOpt (body x)).length + (encBool (body x).isNone).length + 1)
+        ≤ c * (t a + s a + 1) := by
+    refine ⟨cN * (3 * W + 1), fun a n x hx => ?_⟩
+    rw [hencBoolLen]
+    exact nat_bound₃ (hu1 a) (hcW cn a hWcn) (hWt a n x hx).2.1 (hcW 1 a hW1)
+  obtain ⟨A2, hA2⟩ : ∃ c, ∀ (a : α) (b : Bool),
+      cC4 * ((encBool b).length + 1) ≤ c * (t a + s a + 1) := by
+    refine ⟨cC4 * (W + 1), fun a b => ?_⟩
+    rw [hencBoolLen]
+    exact nat_bound₁ (hu1 a) (hcW 1 a hW1)
+  obtain ⟨A3, hA3⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cC1 * ((enc x).length + 1) ≤ c * (t a + s a + 1) :=
+    ⟨cC1 * (W + 1), fun a n x hx => nat_bound₁ (hu1 a) (hWt a n x hx).1⟩
+  obtain ⟨A4, hA4⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cD * (cd * ((encOpt (some x)).length + 1) + (encOpt (some x)).length + (enc x).length + 1)
+        ≤ c * (t a + s a + 1) :=
+    ⟨cD * (3 * W + 1), fun a n x hx =>
+      nat_bound₃ (hu1 a) (hWt a n x hx).2.2.2.1 (hWt a n x hx).2.2.1 (hWt a n x hx).1⟩
+  obtain ⟨A5, hA5⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cC3 * ((encOpt (some x)).length + 1) ≤ c * (t a + s a + 1) :=
+    ⟨cC3 * (W + 1), fun a n x hx => nat_bound₁ (hu1 a) (hWt a n x hx).2.2.1⟩
+  obtain ⟨A6, hA6⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cB * (t x + (enc x).length + (encOpt (body x)).length + 1) ≤ c * (t a + s a + 1) :=
+    ⟨cB * (3 * W + 1), fun a n x hx =>
+      nat_bound₃ (hu1 a) (hWt a n x hx).2.2.2.2.2 (hWt a n x hx).1 (hWt a n x hx).2.1⟩
+  obtain ⟨A7, hA7⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cI * (ci * ((enc x).length + 1) + (enc x).length + 1) ≤ c * (t a + s a + 1) := by
+    refine ⟨cI * (2 * W + 1), fun a n x hx => nat_bound₂ (hu1 a) ?_ (hWt a n x hx).1⟩
+    calc ci * ((enc x).length + 1) ≤ ci * (s a + 1) :=
+          Nat.mul_le_mul_left _ (by have := hsize a n x hx; omega)
+      _ ≤ W * (s a + 1) := Nat.mul_le_mul_right _ hWci
+      _ ≤ W * (t a + s a + 1) := hvu a W
+  obtain ⟨B1, hB1⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cN * (0 + (encOpt (body x)).length + (encBool (body x).isNone).length + 1) + K
+        ≤ c * (s a + 1) := by
+    refine ⟨cN * (3 * W + 1) + K, fun a n x hx => nat_bound_add (hv1 a) ?_⟩
+    rw [hencBoolLen]
+    exact nat_bound₃ (hv1 a) (hcWv 0 a (by omega)) (hWlen a n x hx).2.1 (hcWv 1 a hW1)
+  obtain ⟨B2, hB2⟩ : ∃ c, ∀ (a : α) (w : List Bool), w.length ≤ W * (s a + 1) →
+      w.length + 1 + K ≤ c * (s a + 1) :=
+    ⟨W + 1 + K, fun a w hw => nat_bound_add (hv1 a) (nat_bound₀ (hv1 a) hw)⟩
+  obtain ⟨B3, hB3⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cD * (0 + (encOpt (some x)).length + (enc x).length + 1) + K ≤ c * (s a + 1) :=
+    ⟨cD * (3 * W + 1) + K, fun a n x hx => nat_bound_add (hv1 a)
+      (nat_bound₃ (hv1 a) (hcWv 0 a (by omega)) (hWlen a n x hx).2.2.1 (hWlen a n x hx).1)⟩
+  obtain ⟨B4, hB4⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cB * (s x + (enc x).length + (encOpt (body x)).length + 1) + K ≤ c * (s a + 1) :=
+    ⟨cB * (3 * W + 1) + K, fun a n x hx => nat_bound_add (hv1 a)
+      (nat_bound₃ (hv1 a) (hWlen a n x hx).2.2.2.2.1 (hWlen a n x hx).1
+        (hWlen a n x hx).2.1)⟩
+  obtain ⟨B5, hB5⟩ : ∃ c, ∀ a n x, loopIterate body n a = some x →
+      cI * (0 + (enc x).length + 1) + K ≤ c * (s a + 1) :=
+    ⟨cI * (2 * W + 1) + K, fun a n x hx => nat_bound_add (hv1 a)
+      (nat_bound₂ (hv1 a) (hcWv 0 a (by omega)) (hWlen a n x hx).1)⟩
+  -- the cost of one round, and of the whole loop
+  set A : ℕ := A1 + A2 + A3 + A4 + A5 + A6 + A7 + 1 with hAdef
+  set B : ℕ := B1 + 3 * B2 + B3 + B4 + B5 + K + 1 with hBdef
+  -- ### The exit branch: the loop is over, so nothing is left to do
+  have hExit : ∀ p : α × ℕ, TransformsTapes MNop (fun _ ws => PExit p.1 p.2 ws)
+      (fun _ _ ws' => QR p.1 p.2 ws') (A * (t p.1 + s p.1 + 1)) (B * (s p.1 + 1)) := by
+    rintro ⟨a, n⟩
+    refine hMNop.imp (fun _ _ _ => trivial) (fun _ ws ws' hP hQ => ?_) ?_ ?_
+    · rw [hQ]
+      obtain ⟨y, hy, hby, hws⟩ := (hPExit a n ws).mp hP
+      refine (hQR a n ws).mpr ⟨fun z hz _ => ?_, fun z z' hz hbz => ?_⟩
+      · rw [hy] at hz
+        obtain rfl : z = y := (Option.some.inj hz).symm
+        refine ⟨by rw [hws, tapeWords_fst], ?_⟩
+        simp [hws, tapeWords_thd hT14 hT34, hby, hencBoolHead]
+      · rw [hy] at hz
+        obtain rfl : z = y := (Option.some.inj hz).symm
+        rw [hby] at hbz
+        exact absurd hbz (by simp)
+    · calc (1 : ℕ) ≤ 1 * (t a + s a + 1) := by omega
+        _ ≤ A * (t a + s a + 1) := Nat.mul_le_mul_right _ (by omega)
+    · calc K ≤ K * (s a + 1) := Nat.le_mul_of_pos_right _ (by omega)
+        _ ≤ B * (s a + 1) := Nat.mul_le_mul_right _ (by omega)
+  -- ### The continuation branch: one more iteration of the loop body
+  have hCont : ∀ p : α × ℕ, TransformsTapes
+      (MClear4.seq (MClear1.seq (MDestr.seq (MClear3.seq MBody))))
+      (fun _ ws => PCont p.1 p.2 ws) (fun _ _ ws' => QR p.1 p.2 ws')
+      (A * (t p.1 + s p.1 + 1)) (B * (s p.1 + 1)) := by
+    rintro ⟨a, n⟩
+    rcases hit : loopIterate body n a with _ | x
+    · intro input ws cfg _ _ _ hP
+      obtain ⟨y, y', hy, _, _⟩ := (hPCont a n ws).mp hP
+      rw [hit] at hy
+      exact absurd hy (by simp)
+    rcases hb : body x with _ | x'
+    · intro input ws cfg _ _ _ hP
+      obtain ⟨y, y', hy, hby, _⟩ := (hPCont a n ws).mp hP
+      rw [hit] at hy
+      obtain rfl : y = x := (Option.some.inj hy).symm
+      rw [hb] at hby
+      exact absurd hby (by simp)
+    have hx' : loopIterate body (n + 1) a = some x' := by
+      rw [loopIterate_succ', hit]; simpa using hb
+    have hPC : ∀ ws, PCont a n ws →
+        ws = tapeWords T1 T3 T4 (enc x) (encOpt (body x)) (encBool (body x).isNone) := by
+      intro ws hP
+      obtain ⟨y, y', hy, _, hws⟩ := (hPCont a n ws).mp hP
+      rw [hit] at hy
+      obtain rfl : y = x := (Option.some.inj hy).symm
+      exact hws
+    -- clear the flag tape
+    have step4 : TransformsTapes MClear4 (fun _ ws => PCont a n ws)
+        (fun _ _ ws' => ws' = tapeWords T1 T3 T4 (enc x) (encOpt (some x')) [])
+        (cC4 * ((encBool (body x).isNone).length + 1))
+        ((encBool (body x).isNone).length + 1 + K) :=
+      (hMClear4 (encBool (body x).isNone)).imp
+        (fun _ ws hP => by rw [hPC ws hP, tapeWords_thd hT14 hT34])
+        (fun _ ws ws' hP hQ => by
+          rw [hQ, hPC ws hP, update_tapeWords_thd hT14 hT34, hb]) le_rfl le_rfl
+    -- clear the tape holding the current value
+    have step1 : TransformsTapes MClear1
+        (fun _ ws => ws = tapeWords T1 T3 T4 (enc x) (encOpt (some x')) [])
+        (fun _ _ ws' => ws' = tapeWords T1 T3 T4 [] (encOpt (some x')) [])
+        (cC1 * ((enc x).length + 1)) ((enc x).length + 1 + K) :=
+      (hMClear1 (enc x)).imp (fun _ ws hP => by rw [hP, tapeWords_fst])
+        (fun _ ws ws' hP hQ => by rw [hQ, hP, update_tapeWords_fst]) le_rfl le_rfl
+    -- extract the new value from the result of the body
+    have stepD : TransformsTapes MDestr
+        (fun _ ws => ws = tapeWords T1 T3 T4 [] (encOpt (some x')) [])
+        (fun _ _ ws' => ws' = tapeWords T1 T3 T4 (enc x') (encOpt (some x')) [])
+        (cD * (cd * ((encOpt (some x')).length + 1) + (encOpt (some x')).length
+          + (enc x').length + 1))
+        (cD * (0 + (encOpt (some x')).length + (enc x').length + 1) + K) :=
+      (hMDestr x').imp
+        (fun _ ws hP => ⟨by rw [hP, tapeWords_snd hT13]; simp,
+          fun l hl3 _ => by rw [hP]; exact tapeWords_of_ne_snd hl3⟩)
+        (fun _ ws ws' hP hQ => by rw [hQ, hP, update_tapeWords_fst]; simp) le_rfl le_rfl
+    -- clear the tape holding the result of the body
+    have step3 : TransformsTapes MClear3
+        (fun _ ws => ws = tapeWords T1 T3 T4 (enc x') (encOpt (some x')) [])
+        (fun _ _ ws' => ws' = tapeWords T1 T3 T4 (enc x') [] [])
+        (cC3 * ((encOpt (some x')).length + 1)) ((encOpt (some x')).length + 1 + K) :=
+      (hMClear3 (encOpt (some x'))).imp (fun _ ws hP => by rw [hP, tapeWords_snd hT13])
+        (fun _ ws ws' hP hQ => by rw [hQ, hP, update_tapeWords_snd hT13]) le_rfl le_rfl
+    -- run the body on the new value
+    have stepB : TransformsTapes MBody (fun _ ws => ws = tapeWords T1 T3 T4 (enc x') [] [])
+        (fun _ _ ws' => ws' = tapeWords T1 T3 T4 (enc x') (encOpt (body x')) [])
+        (cB * (t x' + (enc x').length + (encOpt (body x')).length + 1))
+        (cB * (s x' + (enc x').length + (encOpt (body x')).length + 1) + K) :=
+      (hMBody x').imp
+        (fun _ ws hP => ⟨by rw [hP, tapeWords_fst],
+          fun l hl1 _ => by rw [hP]; exact tapeWords_of_ne_fst hl1⟩)
+        (fun _ ws ws' hP hQ => by rw [hQ, hP, update_tapeWords_snd hT13]) le_rfl le_rfl
+    refine (transformsTapes_seq step4 (transformsTapes_seq step1 (transformsTapes_seq stepD
+      (transformsTapes_seq step3 stepB (fun _ _ _ _ h => h)) (fun _ _ _ _ h => h))
+      (fun _ _ _ _ h => h)) (fun _ _ _ _ h => h)).imp (fun _ _ h => h)
+      (fun _ ws ws' hP hQ => ?_) ?_ ?_
+    · obtain ⟨_, rfl, _, rfl, _, rfl, _, rfl, hfin⟩ := hQ
+      refine (hQR a n ws').mpr ⟨fun z hz hbz => ?_, fun z z' hz hbz => ?_⟩
+      · rw [hit] at hz
+        obtain rfl : z = x := (Option.some.inj hz).symm
+        rw [hb] at hbz
+        exact absurd hbz (by simp)
+      · rw [hit] at hz
+        obtain rfl : z = x := (Option.some.inj hz).symm
+        rw [hb] at hbz
+        obtain rfl : z' = x' := (Option.some.inj hbz).symm
+        exact ⟨hfin, by rw [hfin, tapeWords_thd hT14 hT34]; simp⟩
+    · have e2 := hA2 a (body x).isNone
+      have e3 := hA3 a n x hit
+      have e4 := hA4 a (n + 1) x' hx'
+      have e5 := hA5 a (n + 1) x' hx'
+      have e6 := hA6 a (n + 1) x' hx'
+      calc _ ≤ A2 * (t a + s a + 1) + (A3 * (t a + s a + 1) + (A4 * (t a + s a + 1)
+              + (A5 * (t a + s a + 1) + A6 * (t a + s a + 1)))) :=
+            Nat.add_le_add e2 (Nat.add_le_add e3 (Nat.add_le_add e4 (Nat.add_le_add e5 e6)))
+        _ = (A2 + A3 + A4 + A5 + A6) * (t a + s a + 1) := by ring
+        _ ≤ A * (t a + s a + 1) := Nat.mul_le_mul_right _ (by omega)
+    · have g2 := hB2 a (encBool (body x).isNone) (by rw [hencBoolLen]; exact hcWv 1 a hW1)
+      have g3 := hB2 a (enc x) (hWlen a n x hit).1
+      have g4 := hB3 a (n + 1) x' hx'
+      have g5 := hB2 a (encOpt (some x')) (hWlen a (n + 1) x' hx').2.2.1
+      have g6 := hB4 a (n + 1) x' hx'
+      calc _ ≤ B2 * (s a + 1) + (B2 * (s a + 1) + (B3 * (s a + 1)
+              + (B2 * (s a + 1) + B4 * (s a + 1)))) :=
+            Nat.add_le_add g2 (Nat.add_le_add g3 (Nat.add_le_add g4 (Nat.add_le_add g5 g6)))
+        _ = (B2 + B2 + B3 + B2 + B4) * (s a + 1) := by ring
+        _ ≤ B * (s a + 1) := Nat.mul_le_mul_right _ (by omega)
+  -- ### One round: compute the flag on `T4` and branch on it
+  obtain ⟨SBr, hSBr, MBranch, hMBranch⟩ :=
+    exists_transformsTapes_branch (J := α × ℕ) T4 true
+      (P₁ := fun p _ ws => PExit p.1 p.2 ws) (P₂ := fun p _ ws => PCont p.1 p.2 ws)
+      (Q := fun p _ _ ws' => QR p.1 p.2 ws')
+      (t₁ := fun p => A * (t p.1 + s p.1 + 1)) (s₁ := fun p => B * (s p.1 + 1))
+      (t₂ := fun p => A * (t p.1 + s p.1 + 1)) (s₂ := fun p => B * (s p.1 + 1)) hExit hCont
+  haveI := hSBr
+  set A' : ℕ := A1 + A + 1 with hA'def
+  set B' : ℕ := B1 + B + K + 1 with hB'def
+  have hRound : ∀ (a : α) (n : ℕ), TransformsTapes (MIsNone.seq MBranch)
+      (fun _ ws => Pround a n ws) (fun _ _ ws' => QR a n ws')
+      (A' * (t a + s a + 1)) (B' * (s a + 1)) := by
+    intro a n
+    rcases hit : loopIterate body n a with _ | x
+    · intro input ws cfg _ _ _ hP
+      obtain ⟨y, hy, _⟩ := (hPround a n ws).mp hP
+      rw [hit] at hy
+      exact absurd hy (by simp)
+    have hPr : ∀ ws, Pround a n ws → ws = tapeWords T1 T3 T4 (enc x) (encOpt (body x)) [] := by
+      intro ws hP
+      obtain ⟨y, hy, hws⟩ := (hPround a n ws).mp hP
+      rw [hit] at hy
+      obtain rfl : y = x := (Option.some.inj hy).symm
+      exact hws
+    have stepN : TransformsTapes MIsNone (fun _ ws => Pround a n ws)
+        (fun _ _ ws' => PMid a n ws')
+        (cN * (cn + (encOpt (body x)).length + (encBool (body x).isNone).length + 1))
+        (cN * (0 + (encOpt (body x)).length + (encBool (body x).isNone).length + 1) + K) :=
+      (hMIsNone (body x)).imp
+        (fun _ ws hP => ⟨by rw [hPr ws hP, tapeWords_snd hT13],
+          fun l hl3 hl1 => by
+            rw [hPr ws hP]; exact tapeWords_of_ne_fst_snd (by simpa using hl1) hl3⟩)
+        (fun _ ws ws' hP hQ =>
+          (hPMid a n ws').mpr ⟨x, hit, by
+            rw [hQ, hPr ws hP, update_tapeWords_thd hT14 hT34]⟩) le_rfl le_rfl
+    refine (transformsTapes_seq stepN (hMBranch (a, n)) (fun _ ws ws' hP hQ => ?_)).imp
+      (fun _ _ h => h) (fun _ ws ws' hP hQ => ?_) ?_ ?_
+    · -- the flag decides which branch is taken
+      obtain ⟨y, hy, hws⟩ := (hPMid a n ws').mp hQ
+      by_cases hflag : (ws' T4).head? = some true
+      · rw [ite_eq_left hflag]
+        rw [hws, tapeWords_thd hT14 hT34, hencBoolHead] at hflag
+        exact (hPExit a n ws').mpr ⟨y, hy, by simpa using hflag, hws⟩
+      · rw [ite_eq_right hflag]
+        rcases hby : body y with _ | y'
+        · exact absurd (by simp [hws, tapeWords_thd hT14 hT34, hby, hencBoolHead]) hflag
+        · exact (hPCont a n ws').mpr ⟨y, y', hy, hby, hws⟩
+    · obtain ⟨w1, -, h2⟩ := hQ
+      exact h2
+    · simp only [max_self]
+      have e1 := hA1 a n x hit
+      calc _ ≤ A1 * (t a + s a + 1) + (A * (t a + s a + 1) + 1 * (t a + s a + 1)) :=
+            Nat.add_le_add e1 (Nat.add_le_add le_rfl (by omega))
+        _ = (A1 + A + 1) * (t a + s a + 1) := by ring
+        _ ≤ A' * (t a + s a + 1) := Nat.mul_le_mul_right _ (by omega)
+    · simp only [max_self]
+      have g1 := hB1 a n x hit
+      calc _ ≤ B1 * (s a + 1) + (B * (s a + 1) + K * (s a + 1)) :=
+            Nat.add_le_add g1 (Nat.add_le_add le_rfl (Nat.le_mul_of_pos_right _ (by omega)))
+        _ = (B1 + B + K) * (s a + 1) := by ring
+        _ ≤ B' * (s a + 1) := Nat.mul_le_mul_right _ (by omega)
+  -- ### The loop: repeat the round until the flag says that the loop is over
+  have hroundOK : ∀ (a : α) (n : ℕ), n < N a → TransformsTapes (MIsNone.seq MBranch)
+      (fun _ ws => Pround a n ws)
+      (fun _ _ ws' => Pround a (n + 1) ws' ∧ (ws' T4).head? ≠ some true)
+      (A' * (t a + s a + 1)) (B' * (s a + 1)) := by
+    intro a n hn
+    refine (hRound a n).imp (fun _ _ h => h) (fun _ ws ws' hP hQ => ?_) le_rfl le_rfl
+    obtain ⟨y, hy, -⟩ := (hPround a n ws).mp hP
+    obtain ⟨y', hby, hy'⟩ := hnext a n hn y hy
+    obtain ⟨-, q2⟩ := (hQR a n ws').mp hQ
+    obtain ⟨hb', hflag⟩ := q2 y y' hy hby
+    exact ⟨(hPround a (n + 1) ws').mpr ⟨y', hy', hb'⟩, hflag⟩
+  have hstopOK : ∀ a : α, TransformsTapes (MIsNone.seq MBranch)
+      (fun _ ws => Pround a (N a) ws)
+      (fun _ _ ws' => ws' T1 = enc (f a) ∧ (ws' T4).head? = some true)
+      (A' * (t a + s a + 1)) (B' * (s a + 1)) := by
+    intro a
+    refine (hRound a (N a)).imp (fun _ _ h => h) (fun _ ws ws' hP hQ => ?_) le_rfl le_rfl
+    exact ((hQR a (N a) ws').mp hQ).1 (f a) (hN a) (hNstop a)
+  obtain ⟨SL, hSL, MLoop, hMLoop⟩ :=
+    exists_transformsTapes_repeat (J := α) T4 true
+      (P := fun a n _ ws => Pround a n ws) (R := fun a _ ws' => ws' T1 = enc (f a))
+      (N := N) (t := fun a => A' * (t a + s a + 1)) (s := fun a => B' * (s a + 1))
+      hroundOK hstopOK
+  haveI := hSL
+  -- ### The prologue: copy the input onto `T1` and run the body once
+  have hPro : ∀ a : α, TransformsTapes (MCopy.seq MBody)
+      (fun input ws => input = enc a ∧ ∀ l, ws l = [])
+      (fun _ _ ws' => Pround a 0 ws') (A * (t a + s a + 1)) (B * (s a + 1)) := by
+    intro a
+    have s1 : TransformsTapes MCopy (fun input ws => input = enc a ∧ ∀ l, ws l = [])
+        (fun _ _ ws' => ws' = tapeWords T1 T3 T4 (enc a) [] [])
+        (cI * (ci * ((enc a).length + 1) + (enc a).length + 1))
+        (cI * (0 + (enc a).length + 1) + K) := by
+      refine (hMCopy a).imp (fun _ ws hP => ⟨hP.1, fun l _ => hP.2 l⟩)
+        (fun _ ws ws' hP hQ => ?_) le_rfl le_rfl
+      have hws : ws = tapeWords T1 T3 T4 [] [] [] := by
+        funext l
+        rw [hP.2 l]
+        by_cases h1 : l = T1
+        · subst h1; rw [tapeWords_fst]
+        · rw [tapeWords_of_ne_fst h1]
+      rw [hQ, hws, update_tapeWords_fst]
+      simp
+    have s2 : TransformsTapes MBody (fun _ ws => ws = tapeWords T1 T3 T4 (enc a) [] [])
+        (fun _ _ ws' => Pround a 0 ws')
+        (cB * (t a + (enc a).length + (encOpt (body a)).length + 1))
+        (cB * (s a + (enc a).length + (encOpt (body a)).length + 1) + K) :=
+      (hMBody a).imp
+        (fun _ ws hP => ⟨by rw [hP, tapeWords_fst],
+          fun l hl1 _ => by rw [hP]; exact tapeWords_of_ne_fst hl1⟩)
+        (fun _ ws ws' hP hQ => (hPround a 0 ws').mpr
+          ⟨a, rfl, by rw [hQ, hP, update_tapeWords_snd hT13]⟩)
+        le_rfl le_rfl
+    refine (transformsTapes_seq s1 s2 (fun _ _ _ _ h => h)).imp (fun _ _ h => h)
+      (fun _ ws ws' hP hQ => ?_) ?_ ?_
+    · obtain ⟨w1, -, h2⟩ := hQ
+      exact h2
+    · calc _ ≤ A7 * (t a + s a + 1) + A6 * (t a + s a + 1) :=
+            Nat.add_le_add (hA7 a 0 a rfl) (hA6 a 0 a rfl)
+        _ = (A7 + A6) * (t a + s a + 1) := by ring
+        _ ≤ A * (t a + s a + 1) := Nat.mul_le_mul_right _ (by omega)
+    · calc _ ≤ B5 * (s a + 1) + B4 * (s a + 1) :=
+            Nat.add_le_add (hB5 a 0 a rfl) (hB4 a 0 a rfl)
+        _ = (B5 + B4) * (s a + 1) := by ring
+        _ ≤ B * (s a + 1) := Nat.mul_le_mul_right _ (by omega)
+  -- ### The whole machine
+  have hMain : ∀ a : α, TransformsTapes ((MCopy.seq MBody).seq MLoop)
+      (fun input ws => input = enc a ∧ ∀ l, ws l = [])
+      (fun _ _ ws' => ws' T1 = enc (f a))
+      (A * (t a + s a + 1) + (N a + 1) * (A' * (t a + s a + 1) + 1))
+      (B * (s a + 1) + (2 * K * (B' * (s a + 1)) + K)) := by
+    intro a
+    refine (transformsTapes_seq (hPro a) (hMLoop a) (fun _ _ _ _ h => h)).imp (fun _ _ h => h)
+      (fun _ ws ws' hP hQ => ?_) le_rfl le_rfl
+    obtain ⟨w1, -, h2⟩ := hQ
+    exact h2
+  obtain ⟨c₀, hc₀⟩ := computableInTimeAndSpace_of_transformsTapes T1 hMain
+  -- ### The final bounds
+  refine ⟨c₀ * (A + A' + 2) + c₀ * (B + 2 * K * B' + K + 2), hc₀.mono (fun a => ?_) (fun a => ?_)⟩
+  · have hl : (enc (f a)).length ≤ s a := hsize a (N a) (f a) (hN a)
+    have h1 : (N a + 1) * (A' * (t a + s a + 1) + 1)
+        ≤ iterBound a * ((A' + 1) * (t a + s a + 1)) := by
+      refine Nat.mul_le_mul (hNle a) ?_
+      calc A' * (t a + s a + 1) + 1 ≤ A' * (t a + s a + 1) + (t a + s a + 1) := by omega
+        _ = (A' + 1) * (t a + s a + 1) := by ring
+    have hkey : A + iterBound a * (A' + 1) + 2 ≤ (A + A' + 2) * (iterBound a + 1) := by
+      have hm1 : iterBound a * (A' + 1) ≤ (A + A' + 2) * iterBound a := by
+        rw [Nat.mul_comm]
+        exact Nat.mul_le_mul_right _ (by omega)
+      have hm2 : (A + A' + 2) * (iterBound a + 1)
+          = (A + A' + 2) * iterBound a + (A + A' + 2) := by ring
+      omega
+    calc c₀ * (A * (t a + s a + 1) + (N a + 1) * (A' * (t a + s a + 1) + 1)
+            + (enc (f a)).length + 1)
+        ≤ c₀ * (A * (t a + s a + 1) + iterBound a * ((A' + 1) * (t a + s a + 1))
+            + (t a + s a + 1) + (t a + s a + 1)) := Nat.mul_le_mul_left _ (by omega)
+      _ = c₀ * ((A + iterBound a * (A' + 1) + 2) * (t a + s a + 1)) := by ring
+      _ ≤ c₀ * (((A + A' + 2) * (iterBound a + 1)) * (t a + s a + 1)) :=
+          Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ hkey)
+      _ = c₀ * (A + A' + 2) * (iterBound a + 1) * (t a + s a + 1) := by ring
+      _ ≤ _ := Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (by omega))
+  · have hl : (enc (f a)).length ≤ s a := hsize a (N a) (f a) (hN a)
+    have hK1 : K ≤ K * (s a + 1) := Nat.le_mul_of_pos_right _ (by omega)
+    calc c₀ * (B * (s a + 1) + (2 * K * (B' * (s a + 1)) + K) + (enc (f a)).length + 1)
+        ≤ c₀ * (B * (s a + 1) + (2 * K * (B' * (s a + 1)) + K * (s a + 1))
+            + (s a + 1) + (s a + 1)) := Nat.mul_le_mul_left _ (by omega)
+      _ = c₀ * (B + 2 * K * B' + K + 2) * (s a + 1) := by ring
+      _ ≤ _ := Nat.mul_le_mul_right _ (by omega)
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Tuple.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Tuple.lean
new file mode 100644
index 0000000000..5091d7701b
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Tuple.lean
@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Tactic.Ring
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Concat
+
+/-!
+# Complexity of a generic constructor
+
+A non-recursive inductive type is a finite sum of finite products,
+`γ ≅ Σ (i : ι), Π (j : Fin kᵢ), A i j`, so its constructors and its eliminator are the introduction
+rule of a finite product and the elimination rule of a finite coproduct. This file is the first of
+those; `Cslib.Computability.Machines.Turing.MultiTape.Combinators.Ite` is the second.
+
+Both take a single pair of bounds covering every field resp. every branch, and conclude with the
+same bounds up to a constant factor. Separate per-field bounds are recovered by weakening each of
+them to their sum before applying this, so nothing is lost; and since `k` is a constant of the
+type, weakening to their maximum would do just as well. That is why the sum and the supremum do not
+have to be distinguished here, even though every field is computed and only one branch is: the
+distinction is a constant factor as long as the number of items is fixed by the type, and it
+becomes real only for a *variable* number of them, which is
+`Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop`.
+
+The nesting below is a device of the proof and not something the machine does — it runs the `k`
+machines one after the other. Unlike on the eliminator side, where the nested form had to
+renormalise the bounds at every step and the `k`-ary case is therefore the primitive, here the
+induction survives the collapse to a single bound.
+
+The tag of a constructor needs no work: it is a fixed string, and prefixing an encoding with a
+fixed string is again an encoding, so `computableInTimeAndSpace_concat`'s hypothesis absorbs it.
+A constructor with no fields is a constant, which is the base case of the induction.
+
+## What this does not cover
+
+The number of fields has to be a constant of the type. Each nesting costs one rewind of the input
+tape, so `k` fields cost `k` times the input length in time; that is absorbed into the existential
+constant only because `k` is fixed. A structure with a variable number of components — a list, a
+tree — is not a finite product and needs the loop of
+`Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop` with an iteration bound instead.
+That is the same boundary as for the eliminator, where a recursive type needs a fold rather than a
+case analysis.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_flatten`: finitely many computations, concatenated.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_ctor`: the same read as a constructor, for any
+  encoding that is the concatenation of the encoded fields.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α δ : Type*}
+
+/-- **Concatenating finitely many computations.** One pair of bounds covers every field; the cost
+is that pair, plus one rewind of the input tape per field, up to a constant factor that absorbs the
+number of fields. -/
+public theorem computableInTimeAndSpace_flatten {encIn : α ↪ List Bool}
+    {k : ℕ} {fs : Fin k → α → List Bool} {t s : α → ℕ}
+    (hfs : ∀ j, ComputableInTimeAndSpace (fs j) encIn (Function.Embedding.refl (List Bool)) t s) :
+    ∃ c, ComputableInTimeAndSpace (fun a => (List.ofFn fun j => fs j a).flatten) encIn
+      (Function.Embedding.refl (List Bool))
+      (fun a => c * (t a + (encIn a).length + 1))
+      (fun a => c * (s a + 1)) := by
+  induction k with
+  | zero =>
+    -- no fields: the result is the empty string
+    obtain ⟨c, hc⟩ := computableInTimeAndSpace_of_const (α := α) (encIn := encIn)
+      (encOut := Function.Embedding.refl (List Bool)) ([] : List Bool)
+    refine ⟨c, hc.mono (fun a => ?_) (fun a => ?_)⟩
+    · simpa using Nat.le_mul_of_pos_right c (by omega)
+    · simp
+  | succ k ih =>
+    -- one more field, concatenated in front of the rest
+    obtain ⟨c₀, hc₀⟩ := ih (fs := fun j => fs j.succ) fun j => hfs j.succ
+    obtain ⟨c₁, hc₁⟩ := computableInTimeAndSpace_concat
+      (h := fun a => fs 0 a ++ (List.ofFn fun j => fs j.succ a).flatten)
+      (encD := Function.Embedding.refl (List Bool)) (fun _ => rfl) (hfs 0) hc₀
+    have hfun : (fun a => fs 0 a ++ (List.ofFn fun j => fs j.succ a).flatten) =
+        fun a => (List.ofFn fun j => fs j a).flatten := by
+      funext a
+      rw [List.ofFn_succ]
+      rfl
+    rw [hfun] at hc₁
+    refine ⟨c₀ + c₁ + 3, hc₁.mono (fun a => ?_) (fun a => ?_)⟩
+    · have hexp : (c₀ + c₁ + 3) * (t a + (encIn a).length + 1)
+          = c₀ * (t a + (encIn a).length + 1) + c₁ * (t a + (encIn a).length + 1)
+            + 3 * (t a + (encIn a).length + 1) := by ring
+      omega
+    · have hle : c₁ ≤ c₁ * (s a + 1) := Nat.le_mul_of_pos_right _ (by omega)
+      have hexp : (c₀ + c₁ + 3) * (s a + 1)
+          = c₀ * (s a + 1) + c₁ * (s a + 1) + 3 * (s a + 1) := by ring
+      omega
+
+/-- **Complexity of a generic constructor.** If every field is computable and the encoding of the
+constructed value is the concatenation of the encoded fields, then the constructor is computable.
+
+Nothing is asked of the encoding beyond `henc`: building a value needs no computability assumption
+on its encoding, unlike taking one apart, which is why the destructors of a type are collected as
+requirements in `Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option` and its kin while
+the constructors are not. -/
+public theorem computableInTimeAndSpace_ctor {k : ℕ} {A : Fin k → Type*}
+    {fs : (j : Fin k) → α → A j} {h : α → δ}
+    {encIn : α ↪ List Bool} {encA : (j : Fin k) → A j ↪ List Bool} {encD : δ ↪ List Bool}
+    {t s : α → ℕ}
+    (henc : ∀ a, encD (h a) = (List.ofFn fun j => encA j (fs j a)).flatten)
+    (hfs : ∀ j, ComputableInTimeAndSpace (fs j) encIn (encA j) t s) :
+    ∃ c, ComputableInTimeAndSpace h encIn encD
+      (fun a => c * (t a + (encIn a).length + 1))
+      (fun a => c * (s a + 1)) := by
+  obtain ⟨c, hc⟩ := computableInTimeAndSpace_flatten (encIn := encIn)
+    (fs := fun j a => encA j (fs j a)) (t := t) (s := s)
+    fun j => (hfs j).congr (fun _ => rfl) fun _ => rfl
+  exact ⟨c, hc.congr (fun _ => rfl) henc⟩
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/While.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/While.lean
new file mode 100644
index 0000000000..c267bba3db
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/While.lean
@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Ite
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop
+
+/-!
+# While combinator
+
+This file defines the partial function computed by a `while` loop
+
+```
+while cond a do a := step a
+return a
+```
+
+and gives two characterisations of it. It is the version of `loopFunction` with an explicit loop
+condition; the complexity result is derived from the one for `loopFunction` by fusing the condition
+and the body into a single function.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.whileFunction`: the partial function computed by the loop, the `loopFunction`
+  of the fused body. It is undefined on the inputs for which the loop diverges.
+* `Turing.MultiTapeTM.WhileRel`: the graph of the loop, defined inductively.
+
+## Main results
+
+* `Turing.MultiTapeTM.mem_whileFunction`: `whileFunction` is characterised by `WhileRel`.
+* `Turing.MultiTapeTM.whileRel_iff_iterate`: `WhileRel cond step a b` holds exactly if `b` is the
+  first iterate of `step` starting from `a` that does not satisfy `cond`.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_optionIte`: the condition and the body of a loop can
+  be fused into a single function.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_whileFunction`: the complexity of a while loop,
+  obtained from `computableInTimeAndSpace_optionIte` and `computableInTimeAndSpace_loopFunction`.
+-/
+
+namespace Turing.MultiTapeTM
+
+variable {α : Type*} {cond : α → Bool} {step : α → α}
+
+/-- The partial function computed by `while cond do step`. It is defined exactly on the inputs
+for which the loop terminates. -/
+public def whileFunction (cond : α → Bool) (step : α → α) : α →. α :=
+  loopFunction fun a => if cond a then some (step a) else none
+
+/-- The graph of the loop `while cond do step`: `WhileRel cond step a b` means that running the
+loop from the state `a` terminates in the state `b`. -/
+public inductive WhileRel (cond : α → Bool) (step : α → α) : α → α → Prop
+  /-- The loop condition does not hold, so the loop exits immediately. -/
+  | done {a : α} (h : cond a = false) : WhileRel cond step a a
+  /-- The loop condition holds, so the loop runs its body once and continues. -/
+  | loop {a b : α} (h : cond a = true) (hb : WhileRel cond step (step a) b) : WhileRel cond step a b
+
+/-- The graph of `whileFunction` is `WhileRel`. -/
+public theorem mem_whileFunction {a b : α} :
+    b ∈ whileFunction cond step a ↔ WhileRel cond step a b := by
+  have hnone {c : α} : (if cond c then some (step c) else none) = none ↔ cond c = false := by
+    simp
+  have hmem {c d : α} : d ∈ (if cond c then some (step c) else none) ↔
+      cond c = true ∧ d = step c := by
+    cases h : cond c <;> simp [eq_comm]
+  rw [whileFunction, loopFunction, StateTransition.mem_eval]
+  constructor
+  · rintro ⟨hreach, hstop⟩
+    induction hreach using Relation.ReflTransGen.head_induction_on with
+    | refl => exact .done (hnone.mp hstop)
+    | head hstep _ ih =>
+      obtain ⟨hcond, rfl⟩ := hmem.mp hstep
+      exact .loop hcond ih
+  · intro hrel
+    induction hrel with
+    | done h => exact ⟨.refl, hnone.mpr h⟩
+    | loop h _ ih => exact ⟨.head (hmem.mpr ⟨h, rfl⟩) ih.1, ih.2⟩
+
+/-- The loop terminates in the first iterate of its body that does not satisfy the loop
+condition. -/
+public theorem whileRel_iff_iterate {a b : α} :
+    WhileRel cond step a b ↔
+      ∃ n, (∀ i < n, cond (step^[i] a) = true) ∧ cond (step^[n] a) = false ∧ b = step^[n] a := by
+  constructor
+  · intro hrel
+    induction hrel with
+    | done h => exact ⟨0, by simp, by simpa using h, rfl⟩
+    | loop h _ ih =>
+      obtain ⟨n, hlt, hn, rfl⟩ := ih
+      refine ⟨n + 1, ?_, by rw [Function.iterate_succ_apply]; exact hn, ?_⟩
+      · rintro (_ | i) hi
+        · simpa using h
+        · rw [Function.iterate_succ_apply]
+          exact hlt i (by omega)
+      · rw [Function.iterate_succ_apply]
+  · rintro ⟨n, hlt, hn, rfl⟩
+    induction n generalizing a with
+    | zero => exact .done (by simpa using hn)
+    | succ n ih =>
+      refine .loop (by simpa using hlt 0 (by omega)) (ih ?_ ?_)
+      · intro i hi
+        rw [← Function.iterate_succ_apply]
+        exact hlt (i + 1) (by omega)
+      · rw [← Function.iterate_succ_apply]
+        exact hn
+
+/-- The graph of `whileFunction`, in terms of the iterates of the loop body. -/
+public theorem mem_whileFunction_iff_iterate {a b : α} :
+    b ∈ whileFunction cond step a ↔
+      ∃ n, (∀ i < n, cond (step^[i] a) = true) ∧ cond (step^[n] a) = false ∧ b = step^[n] a := by
+  rw [mem_whileFunction, whileRel_iff_iterate]
+
+/-- If one iteration of the loop body makes the encoding grow by at most `growth`, then after `i`
+iterations it has grown by at most `i * growth`. This is one way of obtaining the bound on the
+intermediate values required by `computableInTimeAndSpace_whileFunction`. -/
+public theorem length_enc_iterate_le {enc : α ↪ List Bool} {growth : ℕ}
+    (hgrowth : ∀ a, (enc (step a)).length ≤ (enc a).length + growth) (a : α) (i : ℕ) :
+    (enc (step^[i] a)).length ≤ (enc a).length + i * growth := by
+  induction i with
+  | zero => simp
+  | succ i ih =>
+    rw [Function.iterate_succ_apply']
+    calc (enc (step (step^[i] a))).length ≤ (enc (step^[i] a)).length + growth := hgrowth _
+      _ ≤ (enc a).length + i * growth + growth := by omega
+      _ = (enc a).length + (i + 1) * growth := by rw [Nat.succ_mul]; omega
+
+/-- **Fusing the condition and the body of a loop into a single function.** This is a consequence
+of `computableInTimeAndSpace_cond`, of `IsOptionEncoding.constructor_computable` composed with
+`step` via `computableInTimeAndSpace_comp` (for the `some` branch), and of
+`computableInTimeAndSpace_of_const` (for the constant `none` branch); no reasoning about machines
+is needed. The length of the encoding of the new value enters the bounds because the composition
+has to store it on a work tape. -/
+proof_wanted computableInTimeAndSpace_optionIte
+    {α : Type*} {cond : α → Bool} {step : α → α}
+    {enc : α ↪ List Bool} {encOpt : Option α ↪ List Bool} {encBool : Bool ↪ List Bool}
+    {tc sc ts ss : α → ℕ} (henc : IsOptionEncoding enc encOpt)
+    (hcond : ComputableInTimeAndSpace cond enc encBool tc sc)
+    (hstep : ComputableInTimeAndSpace step enc enc ts ss) :
+    ∃ c, ComputableInTimeAndSpace (fun a => if cond a then some (step a) else none) enc encOpt
+      (fun a => c * (tc a + ts a + (enc (step a)).length + 1))
+      (fun a => c * (sc a + ss a + (enc (step a)).length + 1))
+
+/-- **Complexity of a while loop.**
+
+Assume that
+* `f` picks, for every input, a value at which the loop terminates (`hf`), and the loop started at
+  `a` needs at most `iterBound a` iterations (`hiter`);
+* `cond` and `step` are both computable in time `t` and space `s` (`hcond`, `hstep`), where `s`
+  also bounds the encoded length of all the values encountered while running the loop (`hsize`;
+  note that this includes `a` itself, and see `length_enc_iterate_le` for how to obtain such a
+  bound from a per-iteration growth bound);
+* these bounds do not increase along the iterations of the loop (`ht`, `hs`).
+
+Then `f` is computable in time proportional to the number of iterations times the cost of one
+iteration, and in space proportional to the space of one iteration.
+
+This is obtained from `computableInTimeAndSpace_optionIte`, which fuses `cond` and `step` into a
+single body function, and `computableInTimeAndSpace_loopFunction`, which implements the loop for a
+fused body; `whileFunction` is by definition the `loopFunction` of the fused body. No machine is
+constructed here.
+
+As in `computableInTimeAndSpace_loopFunction`, `hsize` is a genuine additional assumption on `s`,
+since the space bound of `step` does not bound the length of its output. Since the resulting bounds
+are stated up to a constant factor, using a single `s` for all three purposes is no weaker than
+using three separate bounds, whose maximum `s` can be taken to be, and likewise for using a single
+time bound for `cond` and `step`. -/
+proof_wanted computableInTimeAndSpace_whileFunction
+    {α : Type*} {cond : α → Bool} {step : α → α} {f : α → α}
+    {enc : α ↪ List Bool} {encOpt : Option α ↪ List Bool} {encBool : Bool ↪ List Bool}
+    {t s iterBound : α → ℕ}
+    (hf : ∀ a, f a ∈ whileFunction cond step a)
+    (hiter : ∀ a, ∃ m ≤ iterBound a, cond (step^[m] a) = false)
+    (hsize : ∀ a i, (enc (step^[i] a)).length ≤ s a)
+    (henc : IsOptionEncoding enc encOpt)
+    (hcond : ComputableInTimeAndSpace cond enc encBool t s)
+    (hstep : ComputableInTimeAndSpace step enc enc t s)
+    (ht : ∀ a i, t (step^[i] a) ≤ t a) (hs : ∀ a i, s (step^[i] a) ≤ s a) :
+    ∃ c, ComputableInTimeAndSpace f enc enc
+      (fun a => c * (iterBound a + 1) * (t a + s a + 1))
+      (fun a => c * (s a + 1))
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 3d460e45a0..ebe965ce3e 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
@@ -12,7 +12,7 @@ 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 Mathlib.Basic.Sign.Defs
 public import Cslib.Foundations.Data.RelatesInSteps
 
 /-!
@@ -164,6 +164,14 @@ structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where
   output : List Symbol
 deriving Inhabited
 
+/-- Two configurations of a machine without work tapes are equal if their states, input head
+positions and outputs are equal. -/
+lemma Cfg.ext_zero_tapes {Symbol State : Type*} {input : List Symbol}
+    {cfg₁ cfg₂ : Cfg 0 Symbol State input} (state : cfg₁.state = cfg₂.state)
+    (inputPos : cfg₁.inputPos = cfg₂.inputPos) (output : cfg₁.output = cfg₂.output) :
+    cfg₁ = cfg₂ :=
+  Cfg.ext state inputPos (funext fun i => i.elim0) (funext fun i => i.elim0) output
+
 /-- 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.
@@ -384,43 +392,120 @@ def ComputesInTimeAndSpace
   (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
-length `n` it uses at most `t n` steps and `s n` space. It assumes an embedding function
-from the input/output alphabet into the machine alphabet.
+/-- A Turing machine `tm` computes the function `f`, relative to encodings of its input and output
+type into strings over the tape alphabet, using at most `t a` steps and `s a` space on input `a`.
+
 Note that this does not require the alphabet or state set to be finite. -/
 def ComputesFunInTimeAndSpace
+    {α β : Type*}
     (tm : MultiTapeTM k Symbol State)
-    {IOSymbol : Type*}
-    (f : List IOSymbol → List IOSymbol)
-    (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'
+    (encIn : α ↪ List Symbol)
+    (encOut : β ↪ List Symbol)
+    (f : α → β)
+    (t s : α → ℕ) : Prop :=
+  ∀ a, ∃ t' ≤ t a, ∃ s' ≤ s a,
+  ComputesInTimeAndSpace tm (encIn a) (encOut (f a)) 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
-work alphabet and finite state set) via an alphabet embedding function `toMachineSymbol`,
-such that on all inputs of length `n`, `tm` uses at most `t n` steps and at most `s n` space. -/
-def ComputableInTimeAndSpace
-    {IOSymbol : Type*}
-    (f : List IOSymbol → List IOSymbol)
+the function `f` is computable by some multi-tape Turing machine with binary tape alphabet and
+finite state set, relative to the encodings `encIn` and `encOut` of its input and output type,
+using at most `t a` steps and at most `s a` space on input `a`. -/
+def ComputableInTimeAndSpace {α β : Type*}
+    (f : α → β)
+    (encIn : α ↪ List Bool)
+    (encOut : β ↪ List Bool)
+    (t s : α → ℕ) : Prop :=
+  ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State),
+  ComputesFunInTimeAndSpace tm encIn encOut f t s
+
+/-- The variant of `ComputableInTimeAndSpace` in which the bounds depend only on the length of the
+encoded input. This is the notion used to define complexity classes, since those are defined by
+the asymptotics of the bounds in the input length. -/
+abbrev ComputableInTimeAndSpaceOfLength {α β : Type*}
+    (f : α → β)
+    (encIn : α ↪ List Bool)
+    (encOut : β ↪ List Bool)
     (t s : ℕ → ℕ) : Prop :=
-  ∃ (k sym state : ℕ) (toMachineSymbol : _) (tm : MultiTapeTM k (Fin sym) (Fin state)),
-  ComputesFunInTimeAndSpace tm f toMachineSymbol t s
+  ComputableInTimeAndSpace f encIn encOut
+    (fun a => t (encIn a).length) (fun a => s (encIn a).length)
+
+/-- Weakening of the resource bounds of `ComputesFunInTimeAndSpace`. -/
+theorem ComputesFunInTimeAndSpace.mono {α β : Type*}
+    {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol}
+    {f : α → β} {t s t' s' : α → ℕ}
+    (h : ComputesFunInTimeAndSpace tm encIn encOut f t s)
+    (ht : ∀ a, t a ≤ t' a) (hs : ∀ a, s a ≤ s' a) :
+    ComputesFunInTimeAndSpace tm encIn encOut f t' s' := fun a => by
+  obtain ⟨t₀, ht₀, s₀, hs₀, hcomp⟩ := h a
+  exact ⟨t₀, ht₀.trans (ht a), s₀, hs₀.trans (hs a), hcomp⟩
+
+/-- Weakening of the resource bounds of `ComputableInTimeAndSpace`. In particular, bounds that are
+dominated by bounds on the encoded input length give `ComputableInTimeAndSpaceOfLength`. -/
+theorem ComputableInTimeAndSpace.mono {α β : Type*}
+    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t s t' s' : α → ℕ}
+    (h : ComputableInTimeAndSpace f encIn encOut t s)
+    (ht : ∀ a, t a ≤ t' a) (hs : ∀ a, s a ≤ s' a) :
+    ComputableInTimeAndSpace f encIn encOut t' s' := by
+  obtain ⟨k, State, _, tm, htm⟩ := h
+  exact ⟨k, State, ‹_›, tm, htm.mono ht hs⟩
+
+/-- Computability only depends on the two bit strings `encIn a` and `encOut (f a)`, so a
+computation can be read as a computation of a different function at different encodings, as long
+as those strings are the same.
+
+This is what makes destructors composable: a machine computing `body : α → Option α` at an
+encoding of `Option α` is, on inputs where the result is `some x`, literally a machine computing
+`x` at the encoding of `α` induced by `some`. -/
+theorem ComputableInTimeAndSpace.congr {α β γ : Type*}
+    {encIn encIn' : α ↪ List Bool} {encOut : β ↪ List Bool} {encOut' : γ ↪ List Bool}
+    {f : α → β} {g : α → γ} {t s : α → ℕ}
+    (h : ComputableInTimeAndSpace f encIn encOut t s)
+    (hin : ∀ a, encIn' a = encIn a) (hout : ∀ a, encOut' (g a) = encOut (f a)) :
+    ComputableInTimeAndSpace g encIn' encOut' t s := by
+  obtain ⟨k, State, _, tm, htm⟩ := h
+  refine ⟨k, State, ‹_›, tm, fun a => ?_⟩
+  rw [hin a, hout a]
+  exact htm a
+
+/-- The output grows by at most one symbol per step. -/
+theorem length_output_runFrom_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]
+    have : (tm.outputSymbol (tm.runFrom cfg t)).toList.length ≤ 1 := by
+      cases tm.outputSymbol (tm.runFrom cfg t) <;> simp
+    omega
+
+/-- A machine emits at most one symbol per step, so the encoded result of a computation is no
+longer than its time bound. This is the only bound available on the length of an intermediate
+result: a machine can produce an output much longer than the space it uses. -/
+theorem ComputableInTimeAndSpace.length_encOut_le {α β : Type*}
+    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t s : α → ℕ}
+    (h : ComputableInTimeAndSpace f encIn encOut t s) (a : α) :
+    (encOut (f a)).length ≤ t a := by
+  obtain ⟨k, State, _, tm, htm⟩ := h
+  obtain ⟨t', ht', s', _, _, hout, _⟩ := htm a
+  have hlen := length_output_runFrom_le tm (tm.initCfg (encIn a)) t'
+  rw [hout] at hlen
+  simp only [initCfg, List.length_nil, Nat.zero_add] at hlen
+  omega
 
 open Classical in
 /-- The indicator function of a language. -/
-noncomputable def indicator {Symbol : Type*} [Inhabited Symbol] (L : Language Symbol) :
-    List Symbol → List Symbol
-  | x => if x ∈ L then [default] else []
+noncomputable def indicator {α : Type*} (L : Set α) : α → Bool
+  | x => if x ∈ L then true else false
 
 /-- A language is decidable in time `t` and space `s` if and only if its indicator function
 is computable in time `t` and space `s`. -/
 def DecidableInTimeAndSpace
-    {IOSymbol : Type} [Inhabited IOSymbol]
-    (L : Language IOSymbol)
+    {α : Type}
+    (L : Set α)
+    (enc : α ↪ List Bool)
     (t s : ℕ → ℕ) : Prop :=
-  ComputableInTimeAndSpace (indicator L) t s
+  ComputableInTimeAndSpaceOfLength (indicator L) enc ⟨([·]), by aesop⟩ t s
 
 /-- 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. -/
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Encodings/Option.lean b/Cslib/Computability/Machines/Turing/MultiTape/Encodings/Option.lean
new file mode 100644
index 0000000000..422160ef54
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Encodings/Option.lean
@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant
+
+/-!
+# Encodings of `Option`
+
+A combinator that produces or consumes an `Option` should not prescribe how `Option α` is encoded.
+It is enough that the encoding relates to the encoding of `α` in the way one would expect of a
+tagged union: the constructor `some` and its destructor are computable in linear time and zero
+space, i.e. by streaming the input to the output without using a work tape.
+
+The constructor is stated as computability of `Option.some` itself. There is no such function for
+the destructor, since a total function `Option α → α` would need a junk value at `none`. Instead,
+the destructor is stated as computability of the identity of `α`, read at the encoding of `α`
+induced by `encOpt` via `some` on the input side and at `enc` on the output side. This says exactly
+that the encoding of `some a` can be turned into the encoding of `a`, and says nothing about
+encodings of `none`.
+
+A subtype `{o : Option α // o.isSome}` would be another way of expressing this, but it is not
+needed for composability: computability only depends on the bit strings `encIn a` and
+`encOut (f a)`, so by `ComputableInTimeAndSpace.congr` a machine computing `body : α → Option α`
+is, on the inputs where the result is `some x`, a machine computing `x` at the encoding
+`Function.Embedding.some.trans encOpt`, which is exactly the input encoding of the destructor. The
+subtype would drag `Subtype.val` embeddings and `isSome` proofs through every statement without
+buying anything.
+
+Testing an encoded value for `none` is *not* a requirement: `fun o => o.isNone` is constant except
+at the single argument `none`, so it is computable in constant time and zero space for every
+encoding, by `computableInTimeAndSpace_of_exists_finite_ne`.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.IsOptionEncoding`: the requirements on an encoding of `Option α` relative to
+  an encoding of `α`.
+* `Turing.MultiTapeTM.encOption`: the canonical encoding of `Option α`, which prefixes the encoding
+  of the value with a tag bit.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_isNone`: testing for `none` is computable in
+  constant time and zero space, for every encoding.
+* `Turing.MultiTapeTM.isOptionEncoding_encOption`: the canonical encoding satisfies the
+  requirements.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α : Type*}
+
+/-- The requirements on an encoding `encOpt` of `Option α`, relative to an encoding `enc` of `α`:
+the constructor `some` and its destructor are computable in linear time and zero space. -/
+public structure IsOptionEncoding (enc : α ↪ List Bool) (encOpt : Option α ↪ List Bool) : Prop where
+  /-- The constructor `some` is computable in linear time and zero space. -/
+  constructor_computable : ∃ c, ComputableInTimeAndSpace (Option.some : α → Option α) enc encOpt
+    (fun a => c * ((enc a).length + 1)) (fun _ => 0)
+  /-- The destructor of `some` is computable in linear time and zero space. Note that this only
+  constrains the encodings of values of the form `some a`. -/
+  destructor_computable : ∃ c, ComputableInTimeAndSpace (id : α → α)
+    (Function.Embedding.some.trans encOpt) enc
+    (fun a => c * ((encOpt (some a)).length + 1)) (fun _ => 0)
+
+/-- Testing an encoded value for `none` is computable in constant time and zero space, for every
+encoding of `Option α`, since the function is constant except at the single argument `none`. -/
+public theorem computableInTimeAndSpace_isNone {encOpt : Option α ↪ List Bool}
+    {encBool : Bool ↪ List Bool} :
+    ∃ c, ComputableInTimeAndSpace (fun o : Option α => o.isNone) encOpt encBool
+      (fun _ => c) (fun _ => 0) :=
+  computableInTimeAndSpace_of_exists_finite_ne ⟨false,
+    Set.Finite.subset (Set.finite_singleton none) (by rintro (_ | a) ha <;> simp_all)⟩
+
+/-- The canonical encoding of `Option α`: a tag bit, followed by the encoding of the value. -/
+public def encOption (enc : α ↪ List Bool) : Option α ↪ List Bool where
+  toFun
+    | none => [false]
+    | some a => true :: enc a
+  inj' := by rintro (_ | a) (_ | b) h <;> simp_all
+
+/-- The canonical encoding of `Option α` satisfies the requirements: the constructor emits a `true`
+and then copies its input, the destructor drops the `true` and copies the rest. -/
+proof_wanted isOptionEncoding_encOption {enc : α ↪ List Bool} :
+    IsOptionEncoding enc (encOption enc)
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Encodings/Pair.lean b/Cslib/Computability/Machines/Turing/MultiTape/Encodings/Pair.lean
new file mode 100644
index 0000000000..2da1ae0965
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Encodings/Pair.lean
@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Tactic.Ring
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Concat
+
+/-!
+# Requirements on an encoding of a pair
+
+A combinator that produces or consumes a pair should not prescribe how `α × β` is encoded. What it
+needs is that packing and unpacking are cheap, and nothing about the shape of the encoded string —
+no assumption that it *is* the concatenation of the components, which would rule out interleaved,
+length-prefixed-in-the-middle or otherwise repackaged layouts.
+
+Following `Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option`, each requirement is
+computability of a unary function, at the bounds a machine can actually meet: **linear time and
+constant space**, that is, by streaming the input to the output with only the finite control. Zero
+space, which is what suffices for `Option`, is too strong here: a single tag bit can be dropped
+while streaming, but finding where a component ends may need the control to keep count.
+
+## The one thing that is not a complexity
+
+`cat_injective` says that the components laid out one after the other determine the pair. This is
+not an assumption about `encP` — it says nothing about `encP` at all — but about `encA` and `encB`:
+the first must be self-delimiting in front of the second. It is unavoidable, because without it
+"the components one after the other" is not an encoding and `pack` cannot even be stated. It is
+also exactly the property a parenthesis- or escape-based encoding is designed to have.
+
+## Producing and consuming are not symmetric
+
+`pack` is what a combinator building a pair needs, and `fst_computable`/`snd_computable` are what a
+combinator taking one apart needs. With a concatenation-style layout the first is free — a machine
+emitting the components one after the other has already produced the pair — while the second is
+not, since the boundary has to be found. That asymmetry is why `Encodings/` has to be consulted at
+all: concatenating is easier than parsing.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.catEncoding`: the components, one after the other.
+* `Turing.MultiTapeTM.IsPairEncoding`: the requirements.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_pair_of_isPairEncoding`: two computable functions
+  can be paired, with no assumption on the shape of the pair's encoding.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α β γ : Type*}
+
+/-- The components of a pair laid out one after the other, as an encoding. That this is injective
+is the self-delimitation of `encA` in front of `encB`, and has to be supplied. -/
+public def catEncoding (encA : α ↪ List Bool) (encB : β ↪ List Bool)
+    (h : Function.Injective fun p : α × β => encA p.1 ++ encB p.2) : α × β ↪ List Bool :=
+  ⟨fun p => encA p.1 ++ encB p.2, h⟩
+
+@[simp]
+public lemma catEncoding_apply {encA : α ↪ List Bool} {encB : β ↪ List Bool} {h} (p : α × β) :
+    catEncoding encA encB h p = encA p.1 ++ encB p.2 := rfl
+
+/-- The requirements on an encoding `encP` of `α × β`, relative to encodings of the components:
+the pair can be packed from its components and unpacked back into them, in linear time and constant
+space. Nothing is assumed about the shape of `encP`. -/
+public structure IsPairEncoding (encA : α ↪ List Bool) (encB : β ↪ List Bool)
+    (encP : α × β ↪ List Bool) : Prop where
+  /-- The components one after the other determine the pair. Not a condition on `encP`, but the
+  self-delimitation of `encA` in front of `encB`, without which `pack` cannot be stated. -/
+  cat_injective : Function.Injective fun p : α × β => encA p.1 ++ encB p.2
+  /-- Packing: the components, one after the other, can be turned into the encoded pair in linear
+  time and constant space. -/
+  pack : ∃ c, ComputableInTimeAndSpace (fun p : α × β => p)
+    (catEncoding encA encB cat_injective) encP
+    (fun p => c * ((encA p.1).length + (encB p.2).length + 1)) (fun _ => c)
+  /-- The first component can be read back, in linear time and constant space. -/
+  fst_computable : ∃ c, ComputableInTimeAndSpace Prod.fst encP encA
+    (fun p => c * ((encP p).length + 1)) (fun _ => c)
+  /-- The second component can be read back, in linear time and constant space. -/
+  snd_computable : ∃ c, ComputableInTimeAndSpace Prod.snd encP encB
+    (fun p => c * ((encP p).length + 1)) (fun _ => c)
+
+/-- **Complexity of computing a pair, for any encoding meeting the requirements.** Two computable
+functions of the same input can be paired: run the first, rewind, run the second — which produces
+the components one after the other — and then pack.
+
+The encoded components appear in both bounds because the concatenation is handed to the packing
+machine as its input, and `computableInTimeAndSpace_comp` parks an intermediate result on a work
+tape. Where the packing is the identity, that is, where `encP` *is* the concatenation, the last
+step disappears and `computableInTimeAndSpace_pair` gives the sharper bounds. -/
+public theorem computableInTimeAndSpace_pair_of_isPairEncoding
+    {f : α → β} {g : α → γ}
+    {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
+    {encP : β × γ ↪ List Bool} {tf sf tg sg : α → ℕ}
+    (henc : IsPairEncoding encB encC encP)
+    (hf : ComputableInTimeAndSpace f encIn encB tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encC tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun x => (f x, g x)) encIn encP
+      (fun x => c * (tf x + tg x + (encIn x).length
+        + (encB (f x)).length + (encC (g x)).length + 1))
+      (fun x => c * (sf x + sg x + (encB (f x)).length + (encC (g x)).length + 1)) := by
+  obtain ⟨cp, hp⟩ := henc.pack
+  -- run the two machines one after the other: the components land on the output tape in order
+  obtain ⟨c₁, h₁⟩ := computableInTimeAndSpace_concat (h := fun x => (f x, g x))
+    (encD := catEncoding encB encC henc.cat_injective) (fun _ => rfl) hf hg
+  -- then pack
+  obtain ⟨c₂, h₂⟩ := computableInTimeAndSpace_comp h₁ hp
+  refine ⟨c₂ * (cp + c₁ + 4), h₂.mono (fun x => ?_) (fun x => ?_)⟩
+  · simp only [catEncoding_apply, List.length_append]
+    calc _ ≤ c₂ * ((cp + c₁ + 4) * (tf x + tg x + (encIn x).length
+              + (encB (f x)).length + (encC (g x)).length + 1)) := by
+          refine Nat.mul_le_mul_left _ ?_
+          have h1 : cp * ((encB (f x)).length + (encC (g x)).length + 1)
+              ≤ cp * (tf x + tg x + (encIn x).length
+                + (encB (f x)).length + (encC (g x)).length + 1) :=
+            Nat.mul_le_mul_left _ (by omega)
+          have h2 : (cp + c₁ + 4) * (tf x + tg x + (encIn x).length
+                + (encB (f x)).length + (encC (g x)).length + 1)
+              = cp * (tf x + tg x + (encIn x).length
+                  + (encB (f x)).length + (encC (g x)).length + 1)
+                + c₁ * (tf x + tg x + (encIn x).length
+                  + (encB (f x)).length + (encC (g x)).length + 1)
+                + 4 * (tf x + tg x + (encIn x).length
+                  + (encB (f x)).length + (encC (g x)).length + 1) := by ring
+          omega
+      _ = c₂ * (cp + c₁ + 4) * (tf x + tg x + (encIn x).length
+            + (encB (f x)).length + (encC (g x)).length + 1) := by ring
+  · simp only [catEncoding_apply, List.length_append]
+    calc _ ≤ c₂ * ((cp + c₁ + 4) * (sf x + sg x
+              + (encB (f x)).length + (encC (g x)).length + 1)) := by
+          refine Nat.mul_le_mul_left _ ?_
+          have h1 : cp ≤ cp * (sf x + sg x
+              + (encB (f x)).length + (encC (g x)).length + 1) :=
+            Nat.le_mul_of_pos_right _ (by omega)
+          have h2 : c₁ ≤ c₁ * (sf x + sg x
+              + (encB (f x)).length + (encC (g x)).length + 1) :=
+            Nat.le_mul_of_pos_right _ (by omega)
+          have h3 : (cp + c₁ + 4) * (sf x + sg x
+                + (encB (f x)).length + (encC (g x)).length + 1)
+              = cp * (sf x + sg x + (encB (f x)).length + (encC (g x)).length + 1)
+                + c₁ * (sf x + sg x + (encB (f x)).length + (encC (g x)).length + 1)
+                + 4 * (sf x + sg x + (encB (f x)).length + (encC (g x)).length + 1) := by ring
+          omega
+      _ = c₂ * (cp + c₁ + 4) * (sf x + sg x
+            + (encB (f x)).length + (encC (g x)).length + 1) := by ring
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Encodings/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Encodings/README.md
new file mode 100644
index 0000000000..60f5f1f97b
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Encodings/README.md
@@ -0,0 +1,52 @@
+<pre>
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+</pre>
+
+# Requirements on encodings
+
+Complexity is always measured relative to encodings of the types involved. A combinator that is
+proved for one particular encoding is of little use, so the combinators state which properties of
+an encoding they need, and those properties are collected here, one file per type constructor.
+
+## Principles
+
+* **Requirements, not encodings.** A file here does not fix an encoding; it says what makes an
+  encoding usable. The canonical encoding is provided as an example and is proved to satisfy the
+  requirements.
+* **Constructors and destructors.** The requirement for a type constructor is that its
+  constructors and destructors are computable in linear time and zero space, i.e. by streaming the
+  input to the output without using a work tape. This is stated directly as
+  `ComputableInTimeAndSpace` of the identity function, read at the encoding of the type and at the
+  encoding of the components; no separate notion is introduced for it.
+* **Nothing that follows from the general results.** Deciding which constructor an encoded value
+  belongs to does not have to be required if the answer is determined by finitely many exceptions:
+  for `Option`, `fun o => o.isNone` is constant except at the single argument `none`, so it is
+  computable in constant time and zero space for *every* encoding, by
+  `computableInTimeAndSpace_of_exists_finite_ne`.
+
+## Components
+
+### `Option.lean`
+
+`IsOptionEncoding enc encOpt`: the constructor `some` and its destructor are computable in linear
+time and zero space. The constructor is the computability of `Option.some` itself. The destructor
+is the computability of the identity of `α` from `Function.Embedding.some.trans encOpt` to `enc`,
+which says that the encoding of `some a` can be turned into the encoding of `a` and constrains
+nothing about encodings of `none`.
+
+Composing with a destructor does not need a subtype: by `ComputableInTimeAndSpace.congr`,
+computability only depends on the bit strings `encIn a` and `encOut (f a)`, so a machine whose
+result happens to be `some x` is already a machine computing `x` at the encoding induced by `some`.
+
+Recoding a value from one encoding to another is then transported along a computation by
+`computableInTimeAndSpace_comp`, since a recoding is just a computable identity function. Note
+that this costs space: the intermediate result has to be stored on a work tape, because the output
+tape is append-only and cannot be read back.
+
+`encOption` is the canonical encoding, a tag bit followed by the encoding of the value, and
+`isOptionEncoding_encOption` states that it satisfies the requirements.
+
+This is what the loop combinator
+(`Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop`) needs of the encoding of the
+result of its body.
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..42ce8ce1c6
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean
@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Data.List.Infix
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Basic vocabulary for machine plumbing
+
+Combining Turing machines is mostly about moving data between tapes and about running a machine
+on tapes other than the ones it was written for. The statements of these constructions have to
+talk about configurations without mentioning the state of the machine, since the machines that are
+combined all have different state types.
+
+This file provides that vocabulary:
+
+## Main definitions
+
+* `Turing.MultiTapeTM.Cfg.withState`: a configuration with its state replaced, possibly over a
+  different state type.
+* `Turing.MultiTapeTM.Tapes`: the state-erased part of a configuration, i.e. a configuration over
+  the state type `Unit` with state `none`.
+* `Turing.MultiTapeTM.Cfg.AgreesOutside`: two configurations differ at most on a given set of work
+  tapes (and on the output, which can only grow).
+* `Turing.MultiTapeTM.TransformsCfg`: the specification format of the plumbing machines: started in
+  its initial state from a configuration satisfying a precondition, the machine halts within given
+  time and space bounds in a configuration related to the initial one by a postcondition, touching
+  only a given set of work tapes.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k k' : ℕ} {State Symbol : Type*} {input : List Symbol}
+
+/-- The configuration `cfg` with its state replaced by `q`, possibly over a different state
+type. -/
+public 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]
+public lemma Cfg.withState_state {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).state = q := rfl
+
+@[simp]
+public lemma Cfg.withState_inputPos {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).inputPos = cfg.inputPos := rfl
+
+@[simp]
+public lemma Cfg.withState_workTapes {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).workTapes = cfg.workTapes := rfl
+
+@[simp]
+public lemma Cfg.withState_workTapePos {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).workTapePos = cfg.workTapePos := rfl
+
+@[simp]
+public lemma Cfg.withState_output {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).output = cfg.output := rfl
+
+@[simp]
+public lemma Cfg.withState_inputSymbol {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).inputSymbol = cfg.inputSymbol := rfl
+
+@[simp]
+public lemma Cfg.withState_workTapeSymbols {cfg : Cfg k Symbol State input} {State' : Type*}
+    {q : Option State'} : (cfg.withState q).workTapeSymbols = cfg.workTapeSymbols := rfl
+
+@[simp]
+public 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]
+public lemma Cfg.withState_self {cfg : Cfg k Symbol State input} :
+    cfg.withState cfg.state = cfg := rfl
+
+/-- The part of a configuration that does not depend on the machine: the input head position, the
+work tapes, the work tape heads and the output. It is represented as a configuration over the
+state type `Unit`. -/
+public abbrev Tapes (k : ℕ) (Symbol : Type*) (input : List Symbol) := Cfg k Symbol Unit input
+
+/-- The state-erased part of a configuration. -/
+public def Cfg.tapes (cfg : Cfg k Symbol State input) : Tapes k Symbol input := cfg.withState none
+
+/-- `AgreesOutside S tp₁ tp₂` states that `tp₂` differs from `tp₁` at most on the work tapes in `S`
+and on the output, which can only have grown. -/
+public def Cfg.AgreesOutside (S : Finset (Fin k)) (tp₁ tp₂ : Tapes k Symbol input) : Prop :=
+  tp₁.inputPos = tp₂.inputPos ∧ tp₁.output <+: tp₂.output ∧
+    ∀ i ∉ S, tp₁.workTapes i = tp₂.workTapes i ∧ tp₁.workTapePos i = tp₂.workTapePos i
+
+/-- The specification format of the plumbing machines. `TransformsCfg tm S P Q t s` states that,
+started in the state `tm.q₀` from any configuration whose tapes satisfy `P`, the machine `tm` halts
+after at most `t` steps and using at most `s` space, in a configuration whose tapes are related to
+the initial ones by `Q`, and only the work tapes in `S` have been touched.
+
+Note that `t` and `s` are numbers: the dependency on the data on the tapes is expressed by
+quantifying over that data outside of `TransformsCfg`, with `P` pinning it down. -/
+public def TransformsCfg (tm : MultiTapeTM k Symbol State) (S : Finset (Fin k))
+    (P : (input : List Symbol) → Tapes k Symbol input → Prop)
+    (Q : (input : List Symbol) → Tapes k Symbol input → Tapes k Symbol input → Prop)
+    (t s : ℕ) : Prop :=
+  ∀ (input : List Symbol) (cfg : Cfg k Symbol State input),
+    cfg.state = some tm.q₀ → P input cfg.tapes →
+      ∃ t' ≤ t, (tm.runFrom cfg t').state = none ∧
+        Q input cfg.tapes (tm.runFrom cfg t').tapes ∧
+        tm.spaceUsed cfg t' ≤ s ∧
+        Cfg.AgreesOutside S cfg.tapes (tm.runFrom cfg t').tapes
+
+/-- Weakening the bounds of a `TransformsCfg` statement. -/
+proof_wanted TransformsCfg.mono {tm : MultiTapeTM k Symbol State} {S P Q} {t s t' s' : ℕ}
+    (h : TransformsCfg tm S P Q t s) (ht : t ≤ t') (hs : s ≤ s') : TransformsCfg tm S P Q t' s'
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Clean.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Clean.lean
new file mode 100644
index 0000000000..f57a6953c9
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Clean.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+
+/-!
+# Machines that halt cleanly
+
+A machine *halts cleanly* if, whenever it is started in its initial state with blank work tapes and
+all work tape heads at position `0`, it halts in a configuration in which the work tapes are blank
+again and all work tape heads are back at position `0`. The position of the input head and the
+output produced are not constrained: they are part of the specification of the machine, not of the
+plumbing.
+
+Halting cleanly is what makes machines composable: the machine that runs next can assume that it
+starts on blank tapes, without knowing anything about the machine that ran before it.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.Cfg.IsClean`: all work tapes are blank and all work tape heads are at
+  position `0`.
+* `Turing.MultiTapeTM.HaltsClean`: started clean, the machine halts clean.
+
+## Main results
+
+* `Turing.MultiTapeTM.exists_haltsClean_computesFun`: the clean normal form. Every machine can be
+  replaced by one that computes the same function, halts cleanly, and stays within a constant
+  factor of the original time and space bounds.
+
+The construction uses one *shadow tape per work tape*: the machine with `k` work tapes is simulated
+by a machine with `2 * k` work tapes, where writing to tape `i` also writes a marker to tape
+`k + i`, whose head is kept at the same position. When the simulated machine halts, the marked
+region of every tape is walked and erased. Note that:
+
+* erasing "until a blank is found" without the shadow tapes is unsound, since a machine may write
+  blanks inside the region it has used;
+* a single global shadow tape does not work, since the heads of different tapes are at different
+  positions; with one shadow tape per work tape the head positions stay in bijection;
+* the clean-up has to run on all tapes in parallel, otherwise the time is `k * s` instead of `s`.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State : Type*} {input : List Symbol}
+
+/-- A configuration is clean if all its work tapes are blank and all work tape heads are at
+position `0`. -/
+public def Cfg.IsClean (cfg : Cfg k Symbol State input) : Prop :=
+  (∀ (i : Fin k) (z : ℤ), cfg.workTapes i z = none) ∧ ∀ i : Fin k, cfg.workTapePos i = 0
+
+/-- A machine halts cleanly if every halting configuration that it reaches from a clean initial
+configuration is clean. -/
+public def HaltsClean (tm : MultiTapeTM k Symbol State) : Prop :=
+  ∀ (input : List Symbol) (cfg : Cfg k Symbol State input), cfg.state = some tm.q₀ → cfg.IsClean →
+    ∀ t : ℕ, (tm.runFrom cfg t).state = none → (tm.runFrom cfg t).IsClean
+
+/-- The initial configuration is clean. -/
+proof_wanted isClean_initCfg {tm : MultiTapeTM k Symbol State} (input : List Symbol) :
+    (tm.initCfg input : Cfg k Symbol State input).IsClean
+
+/-- **The clean normal form.** Every machine can be replaced by a machine that computes the same
+function, halts cleanly and stays within a constant factor of the original time and space bounds.
+The new machine has twice as many work tapes: one shadow tape per work tape, recording the cells
+that have been written to. -/
+proof_wanted exists_haltsClean_computesFun {Symbol : Type} [Nonempty Symbol] {State : Type}
+    [Finite State] {α β : Type*} {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol}
+    {encOut : β ↪ List Symbol} {f : α → β} {t s : α → ℕ}
+    (h : ComputesFunInTimeAndSpace tm encIn encOut f t s) :
+    ∃ (c : ℕ) (State' : Type) (_ : Finite State') (tm' : MultiTapeTM (2 * k) Symbol State'),
+      HaltsClean tm' ∧
+      ComputesFunInTimeAndSpace tm' encIn encOut f (fun a => c * (t a + 1)) (fun a => c * (s a + 1))
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/LiftTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/LiftTapes.lean
new file mode 100644
index 0000000000..5f05be0d13
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/LiftTapes.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+
+/-!
+# Running a machine on other tapes
+
+A machine that is combined with other machines needs more work tapes than it uses itself, and its
+tapes have to be placed among the tapes of the combined machine. `liftTapes e tm`, for an injection
+`e : Fin k ↪ Fin k'`, runs the `k`-tape machine `tm` on a machine with `k'` work tapes, using tape
+`e i` for tape `i` and leaving all other tapes and their heads untouched.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.Tapes.restrict`: the tapes in the image of `e`, seen as the tapes of a
+  `k`-tape machine.
+
+## Main results
+
+* `Turing.MultiTapeTM.exists_transformsCfg_liftTapes`: a transformation performed by a `k`-tape
+  machine can be performed by a `k'`-tape machine on any `k` of its tapes, in the same time. Note
+  that the space bound grows by `k'`, since every work tape head visits at least one cell.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k k' : ℕ} {Symbol State : Type*} {input : List Symbol}
+
+/-- The tapes of a `k'`-tape configuration in the image of `e`, seen as the tapes of a `k`-tape
+configuration. -/
+public def Tapes.restrict (e : Fin k ↪ Fin k') (tp : Tapes k' Symbol input) :
+    Tapes k Symbol input :=
+  ⟨none, tp.inputPos, fun i => tp.workTapes (e i), fun i => tp.workTapePos (e i), tp.output⟩
+
+/-- **Running a machine on other tapes.** A transformation performed by a `k`-tape machine can be
+performed by a `k'`-tape machine on the tapes selected by `e`, in the same time and with the same
+space, up to the one cell that every one of the `k'` heads visits. The tapes outside the image of
+`e` are untouched, which is already part of `TransformsCfg`. -/
+proof_wanted exists_transformsCfg_liftTapes {tm : MultiTapeTM k Symbol State} {S : Finset (Fin k)}
+    {P : (input : List Symbol) → Tapes k Symbol input → Prop}
+    {Q : (input : List Symbol) → Tapes k Symbol input → Tapes k Symbol input → Prop} {t s : ℕ}
+    (e : Fin k ↪ Fin k') (h : TransformsCfg tm S P Q t s) :
+    ∃ tm' : MultiTapeTM k' Symbol State, TransformsCfg tm' (S.map e)
+      (fun input tp => P input (tp.restrict e))
+      (fun input tp tp' => Q input (tp.restrict e) (tp'.restrict e)) t (s + k')
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OnTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OnTape.lean
new file mode 100644
index 0000000000..a5e3ce7c58
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OnTape.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Clean
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents
+
+/-!
+# Redirecting the input and the output of a machine to work tapes
+
+This is the bridge between the machine level and the function level. A machine that computes a
+function reads its argument from the read-only input tape and writes its result to the append-only
+output tape. To use it inside a bigger machine, its result has to end up on a work tape, and its
+argument may already be on a work tape rather than on the input tape.
+
+Note that there is no need to copy the input onto a work tape: the input tape is read-only, so the
+first machine that is run on the input can simply read it there. Only the results of intermediate
+computations live on work tapes.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.inTape`, `Turing.MultiTapeTM.outTape`: the two extra tapes used by `onTape`
+  to hold the argument and the result of the simulated machine.
+
+## Main results
+
+* `Turing.MultiTapeTM.exists_outputToTape`: a machine computing `f` can be run on the real input
+  tape with its output redirected to a work tape.
+* `Turing.MultiTapeTM.exists_onTape`: a machine computing `f` can be run with a work tape in place
+  of the input tape and a work tape in place of the output tape.
+* `Turing.MultiTapeTM.exists_tapeToOutput`: the contents of a work tape can be emitted as the
+  output of the machine.
+
+The delicate point in `onTape` is the input head of the simulated machine. `tm` believes that it is
+a clamped position in `Fin (n + 2)`: the cells around the input are blank and an outward move there
+does not move the head at all. The head of the work tape `inTape`, however, is an unrestricted
+integer position, so the simulation has to clamp the outward moves itself. Since the contents of
+the tape are a `List Symbol` and therefore blank-free, reading a blank already means "outside the
+input"; the only thing the finite control has to remember in addition is which of the two
+boundaries the head is parked on, since a left move is legal at the left boundary and a right move
+is legal at the right boundary. So a `left | right` flag suffices, and the alphabet does not have
+to be extended. Note also the off-by-one: the input head starts at position `1` of `Fin (n + 2)`,
+whereas a work tape head starts at `0`, so the correspondence is `inputPos = workPos + 1`.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State : Type*} {α β : Type*}
+
+/-- The work tape holding the argument of the machine simulated by `onTape`. -/
+public def inTape (k : ℕ) : Fin (k + 2) := ⟨k, by omega⟩
+
+/-- The work tape holding the result of the machine simulated by `onTape` and `outputToTape`. -/
+public def outTape (k : ℕ) : Fin (k + 2) := ⟨k + 1, by omega⟩
+
+/-- **Redirecting the output to a work tape.** A machine computing `f` can be run on the real input
+tape with its output written to the work tape `outTape k` instead of the output tape. It is started
+on blank tapes and leaves all tapes except `outTape k` blank. -/
+proof_wanted exists_outputToTape {Symbol : Type} {State : Type} [Finite State]
+    {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol}
+    {f : α → β} {t s : α → ℕ} (hclean : HaltsClean tm)
+    (h : ComputesFunInTimeAndSpace tm encIn encOut f t s) :
+    ∃ (c : ℕ) (State' : Type) (_ : Finite State') (tm' : MultiTapeTM (k + 2) Symbol State'),
+      ∀ a : α, TransformsCfg tm' Finset.univ
+        (fun input tp => input = encIn a ∧ tp.inputPos = 1 ∧ tp.IsClean)
+        (fun _ _ tp' => TapeHolds (outTape k) (encOut (f a)) tp' ∧
+          ∀ i : Fin (k + 2), i ≠ outTape k → TapeHolds i [] tp')
+        (c * (t a + 1)) (s a + (encOut (f a)).length + k + 2)
+
+/-- **Running a machine on work tapes.** A machine computing `f` can be run with the work tape
+`inTape k` in place of the input tape and the work tape `outTape k` in place of the output tape.
+The argument is left on `inTape k`, since the caller may still need it. -/
+proof_wanted exists_onTape {Symbol : Type} {State : Type} [Finite State]
+    {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol}
+    {f : α → β} {t s : α → ℕ} (hclean : HaltsClean tm)
+    (h : ComputesFunInTimeAndSpace tm encIn encOut f t s) :
+    ∃ (c : ℕ) (State' : Type) (_ : Finite State') (tm' : MultiTapeTM (k + 2) Symbol State'),
+      ∀ a : α, TransformsCfg tm' Finset.univ
+        (fun _ tp => TapeHolds (inTape k) (encIn a) tp ∧
+          ∀ i : Fin (k + 2), i ≠ inTape k → TapeHolds i [] tp)
+        (fun _ _ tp' => TapeHolds (inTape k) (encIn a) tp' ∧
+          TapeHolds (outTape k) (encOut (f a)) tp' ∧
+          ∀ i : Fin (k + 2), i ≠ inTape k → i ≠ outTape k → TapeHolds i [] tp')
+        (c * (t a + 1)) (s a + (encIn a).length + (encOut (f a)).length + k + 2)
+
+/-- **Emitting a work tape as the output.** There is a machine that appends the contents of a work
+tape to the output tape and clears the work tape, in time linear in its contents. -/
+proof_wanted exists_tapeToOutput (i : Fin k) :
+    ∃ (c : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Symbol State),
+      ∀ w : List Symbol, TransformsCfg tm {i}
+        (fun _ tp => TapeHolds i w tp)
+        (fun _ tp tp' => tp'.output = tp.output ++ w ∧ TapeHolds i [] tp')
+        (c * (w.length + 1)) (w.length + 1)
+
+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..4ef9711a14
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md
@@ -0,0 +1,173 @@
+<pre>
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+</pre>
+
+# Plumbing for multi-tape Turing machines
+
+The [Combinators](../Combinators) directory builds machines that compute functions built from
+other functions (constants, sequential composition of functions, loops, ...). Almost all of the
+work in these constructions is not about the function being computed, but about *plumbing*: moving
+data between tapes, running a machine on tapes other than the ones it was written for, adding tapes
+that a machine does not use, and making sure that a machine leaves the machinery in a state in
+which the next machine can be started.
+
+This directory collects that plumbing, so that the combinators can be assembled from
+function-level statements and a small number of normal forms.
+
+## Design principles
+
+* **Machines, not functions.** The results here are about `runFrom` and configurations, not about
+  `ComputesFunInTimeAndSpace`. The bridge to the function level is made once, in `OnTape`.
+* **Normal forms instead of state surgery.** Rather than reaching into the state space of a given
+  machine, we first bring it into a normal form (halting cleanly, see `Clean`) and then treat it as
+  a black box. This keeps the combinators free of assumptions about the machines they combine.
+* **Costs are constant factors.** Every construction here may cost a constant factor in time and
+  space; this is absorbed by the existential constant of `ComputableInTimeAndSpace`.
+* **As few machine-level results as possible.** The plumbing exists only to prove a handful of
+  function-level combinators, which are the reusable interface:
+  the case analysis `computableInTimeAndSpace_match` (from `exists_branchOnTape`, dispatching on
+  the encoded scrutinee), the composition of functions (from
+  `seq` and `onTape`), and the loop combinator `computableInTimeAndSpace_loopFunction`. Everything
+  else, in particular the whole `while` result, is derived from those without mentioning tapes.
+  The loop is the only combinator that genuinely needs a machine-level branch, since it chooses
+  between continuing the loop and leaving it, which is not a choice between two functions.
+
+## Components
+
+Each file contains the statements of its results as `proof_wanted`s, together with the definitions
+that are needed to state them. The constructions themselves are still missing.
+
+### `Basic.lean`
+
+The vocabulary shared by all of the following: `Cfg.withState`, `Tapes` (the state-erased part of a
+configuration, needed because the machines that are combined all have different state types),
+`Cfg.AgreesOutside` and `TransformsCfg`, the specification format of a plumbing machine: started in
+its initial state from a configuration satisfying a precondition, it halts within given time and
+space bounds in a configuration related to the initial one by a postcondition, touching only a
+given set of work tapes.
+
+### `Sequential.lean` (construction done)
+
+`seq tm₁ tm₂` runs `tm₁` and, when `tm₁` would halt, continues with `tm₂` from the reached
+configuration: input head, work tapes, work-tape heads and the output produced so far are handed
+over unchanged. This is composition of machines as configuration transformers, not composition of
+the computed functions.
+
+* `runFrom_seq` splits a run of `seq tm₁ tm₂` into the two phases (proved),
+* `transformsCfg_seq` composes two `TransformsCfg` statements.
+
+### `LiftTapes.lean`
+
+`exists_transformsCfg_liftTapes`: for an injection `e : Fin k ↪ Fin k'`, a transformation performed
+by a `k`-tape machine can be performed by a `k'`-tape machine on the tapes selected by `e`, leaving
+all other tapes and their heads untouched. Every machine that is combined with another one goes
+through this, since the combined machine has more tapes than its parts. Time is preserved; the
+space bound grows by `k'`, since each of the `k'` heads visits at least one cell.
+
+### `Clean.lean`
+
+`Cfg.IsClean` (all work tapes blank, all work tape heads at `0`) and `HaltsClean` (started clean,
+the machine halts clean). The input head position and the output are not constrained: they belong
+to the specification of the machine, not to the plumbing.
+
+`exists_haltsClean_computesFun` is the normal form: every machine can be replaced by one that
+computes the same function, halts cleanly, and stays within a constant factor of its time and space
+bounds. The construction uses one *shadow tape per work tape* (`k → 2 * k`): writing to a work tape
+also marks the corresponding cell of its shadow tape, and the clean-up walks the marked region and
+erases it. Note that:
+
+* naively erasing "until a blank is found" is unsound, since a machine may write blanks inside the
+  region it has used;
+* a single global shadow tape does not work, since the heads of different tapes are at different
+  positions; with one shadow tape per work tape the head positions stay in bijection, which keeps
+  the simulation lemma cheap;
+* the clean-up must run on all tapes *in parallel*, otherwise the total time is `k * s` rather
+  than `s` per tape.
+
+### `TapeContents.lean`
+
+`TapeHolds i w cfg`: work tape `i` contains exactly `w`, starting at position `0`, blank elsewhere,
+with the head at `0`. In particular `TapeHolds i []` says that the tape is blank and rewound.
+Since the contents are a `List Symbol`, they are blank-free, so a machine can find their end by
+scanning for the first blank.
+
+* `exists_clearTape`: blank a tape and rewind it,
+* `exists_moveTapeTail`: move the contents of a tape, without its first symbol, to a blank tape,
+* `exists_branchOnTape`: behave like one of two machines depending on the symbol under a tape head.
+  Its function-level face is `computableInTimeAndSpace_cond`; it is used directly only by the loop
+  combinator, for the continue flag of a fused loop body.
+
+All of these are linear in the length of the contents and touch only the tapes they are given.
+
+### `Words.lean`
+
+The interface the combinators actually use. `TapesHold ws cfg` says that every work tape holds a
+word, and `TransformsTapes tm P Q t s` is `TransformsCfg` restricted to such configurations, with
+the input head normalised to position `1` and the output left unchanged. Restricting to
+word-holding configurations removes all of the bookkeeping from the combinators: the tapes a
+machine did not touch are described by the postcondition (`ws' l = ws l`) rather than by a set of
+tape indices, so `Cfg.AgreesOutside` never appears, and the configuration is determined by the
+words, so machines compose by reasoning about words only.
+
+Since the bounds are numbers, a specification whose bounds depend on the data is a *family*
+`∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j)` over one fixed machine; `branch` and `repeat` are
+therefore stated over an arbitrary index type, because their machine is built once and specified
+once per index.
+
+Scratch tapes are not exposed. A result of the shape `∃ m c, ∀ k i o keep, …` says that `m` scratch
+tapes suffice, so the caller may use any machine with enough tapes, designating an input tape `i`,
+an output tape `o` and a set `keep` of tapes that have to survive the call; every tape outside
+`keep` is blank before and after.
+
+* `transformsTapes_seq`, `exists_transformsTapes_branch`, `exists_transformsTapes_nop`,
+  `exists_transformsTapes_clear`: composition, branching and the two trivial machines,
+* `exists_transformsTapes_repeat`: running a machine over and over until the first symbol of a tape
+  says the loop is over. This is the loop-back that `seq` cannot express — `seq` sends the halting
+  state of one machine to the initial state of the *next* one, this one sends it back to the
+  initial state of the *same* one — and it is the only reason the loop combinator needs the machine
+  level at all. Its space bound is `2 * k * s + k` rather than `s`, because a round starts with all
+  heads at `0` and heads move by at most one cell per step, so the cells visited by all rounds lie
+  within distance `s` of `0` on each tape,
+* `exists_transformsTapes_ofComputable`, `exists_transformsTapes_ofComputableInput`: evaluating a
+  computable function on work tapes, reading its argument from a work tape resp. from the real
+  input tape. These fold together the clean normal form, `onTape` and `liftTapes`,
+* `computableInTimeAndSpace_of_transformsTapes`: emitting a work tape as the output, which turns a
+  tape transformation back into a computation.
+
+### `OnTape.lean`
+
+The bridge between the machine level and the function level.
+
+* `exists_outputToTape`: run a machine computing `f` on the real input tape, with its output
+  written to a work tape,
+* `exists_onTape`: run it with a work tape in place of the input tape and a work tape in place of
+  the output tape,
+* `exists_tapeToOutput`: emit the contents of a work tape as the output.
+
+There is deliberately no `inputToTape`: the input tape is read-only, so the first machine that is
+run on the input reads it there, and only the results of intermediate computations ever live on
+work tapes.
+
+The delicate point in `onTape` is the input head of the simulated machine, which the machine
+believes to be a clamped position in `Fin (n + 2)`, while the head of a work tape is an
+unrestricted integer position. The simulation therefore has to clamp the outward moves itself.
+Reading a blank already means "outside the input", so the finite control only has to remember which
+of the two boundaries the head is parked on: a `left | right` flag suffices and the alphabet does
+not have to be extended. Note also the off-by-one: the input head starts at position `1`, a work
+tape head at `0`, so the correspondence is `inputPos = workPos + 1`.
+
+## Dependencies
+
+```
+Deterministic, TapeLemmas
+  └── Basic
+        ├── Sequential
+        ├── LiftTapes
+        ├── Clean
+        └── TapeContents
+              └── OnTape   (also needs Clean)
+                    └── Words   (also needs Sequential, LiftTapes)
+```
+
+The combinators use only `Words`; everything below it is what `Words` is to be proved from.
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..6ae348fe81
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean
@@ -0,0 +1,153 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Data.PFun
+public import Mathlib.Data.List.Infix
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+
+/-!
+# Sequential composition of Turing machines
+
+`seq tm₁ tm₂` runs `tm₁` and, instead of halting, continues with `tm₂` on the configuration
+reached by `tm₁`: the input head position, the work tapes, the work tape heads and the output
+produced so far are all handed over unchanged. This is not composition of the computed functions,
+but composition of the machines as transformers of configurations.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.seq`: the sequential composition of two machines.
+* `Turing.MultiTapeTM.Cfg.withState`: a configuration with its state replaced, used to relate
+  configurations of `tm₁` and `tm₂` with those of `seq tm₁ tm₂`.
+
+## Main results
+
+* `Turing.MultiTapeTM.runFrom_seq`: if `tm₁` halts after `t₁` steps, then after `t₁ + t₂` steps
+  `seq tm₁ tm₂` is in the configuration that `tm₂` reaches after `t₂` steps when started in the
+  configuration left behind by `tm₁`.
+-/
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State State₁ State₂ : Type*} {input : List Symbol}
+
+/-- The sequential composition of `tm₁` and `tm₂`: it behaves like `tm₁` until `tm₁` would halt,
+at which point it switches to the initial state of `tm₂` and behaves like `tm₂`. All other
+components of the configuration are left untouched by the switch. -/
+@[expose]
+public 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 with q' := some (action.q'.elim (.inr tm₂.q₀) .inl) }
+    | .inr q₂ =>
+      let action := tm₂.tr q₂ input work
+      { action with q' := action.q'.map .inr }
+
+variable {tm₁ : MultiTapeTM k Symbol State₁} {tm₂ : MultiTapeTM k Symbol State₂}
+
+/-- `seq tm₁ tm₂` starts in the initial configuration of `tm₁`. -/
+@[simp]
+public lemma initCfg_seq (input : List Symbol) :
+    (tm₁.seq tm₂).initCfg input = (tm₁.initCfg input).withState (some (Sum.inl tm₁.q₀)) := rfl
+
+/-- In the second phase, `seq tm₁ tm₂` performs the steps of `tm₂`. -/
+public lemma step_seq_inr (cfg : Cfg k Symbol State₂ input) :
+    (tm₁.seq tm₂).step (cfg.withState (cfg.state.map Sum.inr)) =
+      (tm₂.step cfg).withState ((tm₂.step cfg).state.map Sum.inr) := by
+  cases h : cfg.state with
+  | none => simp [step, h]
+  | some q => refine Cfg.ext ?_ ?_ ?_ ?_ ?_ <;> simp [step, seq, h]
+
+/-- In the second phase, `seq tm₁ tm₂` performs the runs of `tm₂`. -/
+public lemma runFrom_seq_inr (cfg : Cfg k Symbol State₂ input) (t : ℕ) :
+    (tm₁.seq tm₂).runFrom (cfg.withState (cfg.state.map Sum.inr)) t =
+      (tm₂.runFrom cfg t).withState ((tm₂.runFrom cfg t).state.map Sum.inr) := by
+  induction t with
+  | zero => simp [runFrom_zero]
+  | succ t ih =>
+    rw [runFrom_succ_eq_step', ih, step_seq_inr, ← runFrom_succ_eq_step' (tm := tm₂)]
+
+/-- As long as `tm₁` does not halt, `seq tm₁ tm₂` performs the steps of `tm₁`. -/
+public lemma step_seq_inl_of_ne_none {cfg : Cfg k Symbol State₁ input}
+    (h : (tm₁.step cfg).state ≠ none) :
+    (tm₁.seq tm₂).step (cfg.withState (cfg.state.map Sum.inl)) =
+      (tm₁.step cfg).withState ((tm₁.step cfg).state.map Sum.inl) := by
+  cases hcfg : cfg.state with
+  | none => simp [step, hcfg]
+  | some q =>
+    have hq : (tm₁.tr q cfg.inputSymbol cfg.workTapeSymbols).q' ≠ none := by
+      simpa [step, hcfg] using h
+    cases hq' : (tm₁.tr q cfg.inputSymbol cfg.workTapeSymbols).q' with
+    | none => exact absurd hq' hq
+    | some q' => refine Cfg.ext ?_ ?_ ?_ ?_ ?_ <;> simp [step, seq, hcfg, hq']
+
+/-- The step in which `tm₁` halts is the step in which `seq tm₁ tm₂` switches to `tm₂`. -/
+public lemma step_seq_inl_of_halt {cfg : Cfg k Symbol State₁ input} (hcfg : cfg.state ≠ none)
+    (h : (tm₁.step cfg).state = none) :
+    (tm₁.seq tm₂).step (cfg.withState (cfg.state.map Sum.inl)) =
+      (tm₁.step cfg).withState (some (Sum.inr tm₂.q₀)) := by
+  cases hq : cfg.state with
+  | none => exact absurd hq hcfg
+  | some q =>
+    have hq' : (tm₁.tr q cfg.inputSymbol cfg.workTapeSymbols).q' = none := by
+      simpa [step, hq] using h
+    refine Cfg.ext ?_ ?_ ?_ ?_ ?_ <;> simp [step, seq, hq, hq']
+
+/-- As long as `tm₁` does not halt, `seq tm₁ tm₂` performs the runs of `tm₁`. -/
+public lemma runFrom_seq_inl {cfg : Cfg k Symbol State₁ input} {t : ℕ}
+    (h : ∀ τ ≤ t, (tm₁.runFrom cfg τ).state ≠ none) :
+    (tm₁.seq tm₂).runFrom (cfg.withState (cfg.state.map Sum.inl)) t =
+      (tm₁.runFrom cfg t).withState ((tm₁.runFrom cfg t).state.map Sum.inl) := by
+  induction t with
+  | zero => simp [runFrom_zero]
+  | succ t ih =>
+    rw [runFrom_succ_eq_step', ih fun τ hτ => h τ (by omega), runFrom_succ_eq_step' (tm := tm₁)]
+    exact step_seq_inl_of_ne_none (by
+      rw [← runFrom_succ_eq_step']
+      exact h (t + 1) le_rfl)
+
+/-- **Correctness of sequential composition.** If `tm₁` halts after exactly `t₁` steps, then after
+`t₁ + t₂` steps `seq tm₁ tm₂` is in the configuration reached by `tm₂` after `t₂` steps, started
+in the configuration `tm₁` left behind. -/
+public theorem runFrom_seq {cfg : Cfg k Symbol State₁ input} {t₁ : ℕ} (hcfg : cfg.state ≠ none)
+    (hmin : ∀ τ < t₁, (tm₁.runFrom cfg τ).state ≠ none)
+    (hhalt : (tm₁.runFrom cfg t₁).state = none) (t₂ : ℕ) :
+    (tm₁.seq tm₂).runFrom (cfg.withState (cfg.state.map Sum.inl)) (t₁ + t₂) =
+      (tm₂.runFrom ((tm₁.runFrom cfg t₁).withState (some tm₂.q₀)) t₂).withState
+        ((tm₂.runFrom ((tm₁.runFrom cfg t₁).withState (some tm₂.q₀)) t₂).state.map Sum.inr) := by
+  obtain ⟨m, rfl⟩ : ∃ m, t₁ = m + 1 := by
+    cases t₁ with
+    | zero => exact absurd (by simpa [runFrom_zero] using hhalt) hcfg
+    | succ m => exact ⟨m, rfl⟩
+  have hstep : (tm₁.step (tm₁.runFrom cfg m)).state = none := by
+    rwa [← runFrom_succ_eq_step']
+  have hswitch : (tm₁.seq tm₂).runFrom (cfg.withState (cfg.state.map Sum.inl)) (m + 1) =
+      (tm₁.runFrom cfg (m + 1)).withState (some (Sum.inr tm₂.q₀)) := by
+    rw [runFrom_add _ m 1, runFrom_seq_inl (fun τ hτ => hmin τ (by omega)),
+      runFrom_succ_eq_step', runFrom_zero,
+      step_seq_inl_of_halt (hmin m (by omega)) hstep, ← runFrom_succ_eq_step']
+  rw [runFrom_add _ (m + 1) t₂, hswitch]
+  exact runFrom_seq_inr ((tm₁.runFrom cfg (m + 1)).withState (some tm₂.q₀)) t₂
+
+/-- **Sequential composition of two transformations.** If `tm₁` transforms configurations
+satisfying `P₁` into configurations satisfying `Q₁`, and `tm₂` continues from there, then
+`seq tm₁ tm₂` performs both transformations one after the other. -/
+proof_wanted transformsCfg_seq {k : ℕ} {Symbol State₁ State₂ : Type*}
+    {tm₁ : MultiTapeTM k Symbol State₁} {tm₂ : MultiTapeTM k Symbol State₂} {S₁ S₂ : Finset (Fin k)}
+    {P₁ : (input : List Symbol) → Tapes k Symbol input → Prop}
+    {Q₁ Q₂ : (input : List Symbol) → Tapes k Symbol input → Tapes k Symbol input → Prop}
+    {P₂ : (input : List Symbol) → Tapes k Symbol input → Prop} {t₁ s₁ t₂ s₂ : ℕ}
+    (h₁ : TransformsCfg tm₁ S₁ P₁ Q₁ t₁ s₁) (h₂ : TransformsCfg tm₂ S₂ P₂ Q₂ t₂ s₂)
+    (hmid : ∀ input tp tp', P₁ input tp → Q₁ input tp tp' → P₂ input tp') :
+    TransformsCfg (tm₁.seq tm₂) (S₁ ∪ S₂) P₁
+      (fun input tp tp'' => ∃ tp', Q₁ input tp tp' ∧ Q₂ input tp' tp'') (t₁ + t₂) (s₁ + s₂)
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean
new file mode 100644
index 0000000000..a77f872103
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean
@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+
+/-!
+# The contents of a work tape
+
+This file provides the vocabulary for talking about the contents of a single work tape, and the
+machines that manipulate it: clearing a tape, moving the contents of one tape to another, and
+branching on the symbol under a tape head.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.TapeHolds`: work tape `i` contains the word `w` starting at position `0`,
+  is blank everywhere else, and its head is at position `0`. Note that `TapeHolds i []` says that
+  the tape is blank with its head at position `0`.
+
+## Main results
+
+* `Turing.MultiTapeTM.exists_clearTape`: a tape can be blanked in time linear in its contents.
+* `Turing.MultiTapeTM.exists_moveTapeTail`: the contents of a tape, without its first symbol, can
+  be moved to a blank tape in time linear in its contents.
+* `Turing.MultiTapeTM.exists_branchOnTape`: two machines can be combined into one that behaves like
+  the first one if the head of a given tape reads a given symbol, and like the second one
+  otherwise.
+
+Since the contents of a tape are a `List Symbol`, they are blank-free, so the machines can find the
+end of the contents by scanning for the first blank.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State State₁ State₂ : Type*} {input : List Symbol}
+
+/-- Work tape `i` of `cfg` holds the word `w`: the cells `0, …, w.length - 1` contain the symbols
+of `w`, all other cells are blank, and the head is at position `0`. -/
+public def TapeHolds (i : Fin k) (w : List Symbol) (cfg : Cfg k Symbol State input) : Prop :=
+  (∀ (j : ℕ) (h : j < w.length), cfg.workTapes i (j : ℤ) = some (w[j]'h)) ∧
+  (∀ z : ℤ, z < 0 ∨ (w.length : ℤ) ≤ z → cfg.workTapes i z = none) ∧
+  cfg.workTapePos i = 0
+
+/-- **Clearing a tape.** There is a machine that blanks a work tape and returns its head to
+position `0`, in time linear in the contents of the tape. -/
+proof_wanted exists_clearTape (i : Fin k) :
+    ∃ (c : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Symbol State),
+      ∀ w : List Symbol, TransformsCfg tm {i}
+        (fun _ tp => TapeHolds i w tp) (fun _ _ tp' => TapeHolds i [] tp')
+        (c * (w.length + 1)) (w.length + 1)
+
+/-- **Moving the tail of a tape to another tape.** There is a machine that moves the contents of
+tape `src`, without its first symbol, to the blank tape `dst`, clearing `src`, in time linear in
+the contents of `src`. -/
+proof_wanted exists_moveTapeTail {src dst : Fin k} (h : src ≠ dst) :
+    ∃ (c : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Symbol State),
+      ∀ (x : Symbol) (w : List Symbol), TransformsCfg tm {src, dst}
+        (fun _ tp => TapeHolds src (x :: w) tp ∧ TapeHolds dst [] tp)
+        (fun _ _ tp' => TapeHolds src [] tp' ∧ TapeHolds dst w tp')
+        (c * (w.length + 1)) (w.length + 2)
+
+/-- **Branching on the symbol under a tape head.** Two machines performing the same transformation
+under different preconditions can be combined into a machine that behaves like the first one if the
+head of tape `i` reads `x`, and like the second one otherwise. The combined machine needs one extra
+step to read the symbol.
+
+This is the only place where a branch is taken on the contents of a tape. Its function-level face
+is `computableInTimeAndSpace_cond`, which is what should be used everywhere; the branch itself is
+needed here only because the loop combinator branches between continuing the loop and leaving it,
+which is not a choice between two functions. -/
+proof_wanted exists_branchOnTape [DecidableEq Symbol] (i : Fin k) (x : Symbol)
+    {tm₁ : MultiTapeTM k Symbol State₁} {tm₂ : MultiTapeTM k Symbol State₂} {S : Finset (Fin k)}
+    {P₁ P₂ : (input : List Symbol) → Tapes k Symbol input → Prop}
+    {Q : (input : List Symbol) → Tapes k Symbol input → Tapes k Symbol input → Prop}
+    {t₁ s₁ t₂ s₂ : ℕ}
+    (h₁ : TransformsCfg tm₁ S P₁ Q t₁ s₁) (h₂ : TransformsCfg tm₂ S P₂ Q t₂ s₂) :
+    ∃ tm : MultiTapeTM k Symbol (Unit ⊕ State₁ ⊕ State₂), TransformsCfg tm S
+      (fun input tp => if tp.workTapeSymbols i = some x then P₁ input tp else P₂ input tp) Q
+      (max t₁ t₂ + 1) (max s₁ s₂)
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Words.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Words.lean
new file mode 100644
index 0000000000..fdb14d1f9b
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Words.lean
@@ -0,0 +1,251 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Clean
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.LiftTapes
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OnTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents
+
+/-!
+# Machines as transformers of tape words
+
+This file is the interface the combinators use. A combinator never talks about individual cells,
+head positions or the set of tapes a machine has touched: it composes machines that read words
+from some work tapes and write words to others.
+
+`TransformsTapes` is `TransformsCfg` specialised to configurations in which *every* work tape
+holds a word (`TapesHold`), the input head sits at position `1` and the output is left unchanged.
+The specialisation is what makes the combinators cheap to assemble:
+
+* a machine that writes returns the *whole* vector of words: the postcondition of a leaf like
+  `exists_transformsTapes_clear` or `exists_transformsTapes_ofComputable` is a single equality
+  `ws' = Function.update ws o …`, so which tapes survived a step is obtained by rewriting rather
+  than by a case analysis per tape, and `Cfg.AgreesOutside` disappears;
+* the input head and the output are normalised, so sequential composition needs no side
+  conditions;
+* the configuration is determined by the words on the tapes, so two machines can be composed by
+  reasoning about words only.
+
+The bounds `t` and `s` are numbers, as in `TransformsCfg`; a specification whose bounds depend on
+the data is a *family* `∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j)` over one fixed machine.
+This is why `exists_transformsTapes_branch` and `exists_transformsTapes_repeat` are stated over an
+arbitrary index type: the machine has to be built once and specified once per index.
+
+## Scratch tapes
+
+A machine that is run inside a bigger machine needs work tapes of its own. Rather than exposing
+them, the results here quantify over the ambient number of tapes: `∃ m c, ∀ k i o keep, …` says
+that `m` scratch tapes suffice, so the caller may use *any* machine with enough tapes, designating
+an input tape `i`, an output tape `o` and a set `keep` of tapes that have to survive the call. All
+tapes outside `keep` are blank before and after; which of them the machine uses is not observable.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.TapesHold`: every work tape holds a given word.
+* `Turing.MultiTapeTM.TransformsTapes`: the specification format described above.
+
+## Main results
+
+* `Turing.MultiTapeTM.TransformsTapes.imp`: strengthen the precondition, weaken the postcondition
+  and raise the bounds.
+* `Turing.MultiTapeTM.transformsTapes_seq`: sequential composition.
+* `Turing.MultiTapeTM.exists_transformsTapes_branch`: branching on the first symbol of a tape.
+* `Turing.MultiTapeTM.exists_transformsTapes_repeat`: repeating a machine until the first symbol
+  of a tape signals that the loop is over. This is the loop-back that `seq` cannot express, and
+  the only reason the loop combinator needs the machine level at all.
+* `Turing.MultiTapeTM.exists_transformsTapes_nop` and
+  `Turing.MultiTapeTM.exists_transformsTapes_clear`:
+  the two trivial machines.
+* `Turing.MultiTapeTM.exists_transformsTapes_ofComputable`,
+  `Turing.MultiTapeTM.exists_transformsTapes_ofComputableInput`: evaluating a computable function
+  on work tapes, reading its argument from a work tape resp. from the real input tape.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_of_transformsTapes`: emitting a work tape as the
+  output, which turns a tape transformation back into a computation.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State : Type*} {input : List Symbol}
+
+/-- Every work tape of `cfg` holds a word: tape `i` contains `ws i` starting at position `0`, is
+blank everywhere else, and its head is at position `0`. -/
+public def TapesHold (ws : Fin k → List Symbol) (cfg : Cfg k Symbol State input) : Prop :=
+  ∀ i, TapeHolds i (ws i) cfg
+
+/-- `TransformsTapes tm P Q t s` states that, started in its initial state from a configuration
+whose input head is at position `1` and whose work tapes hold words `ws` satisfying `P`, the
+machine `tm` halts after at most `t` steps and using at most `s` space, in a configuration whose
+work tapes hold words `ws'` with `Q input ws ws'`, whose input head is again at position `1` and
+whose output is unchanged. -/
+public def TransformsTapes (tm : MultiTapeTM k Symbol State)
+    (P : (input : List Symbol) → (Fin k → List Symbol) → Prop)
+    (Q : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop)
+    (t s : ℕ) : Prop :=
+  ∀ (input : List Symbol) (ws : Fin k → List Symbol) (cfg : Cfg k Symbol State input),
+    cfg.state = some tm.q₀ → cfg.inputPos = 1 → TapesHold ws cfg → P input ws →
+      ∃ τ ≤ t, ∃ ws', (tm.runFrom cfg τ).state = none ∧
+        Q input ws ws' ∧
+        TapesHold ws' (tm.runFrom cfg τ) ∧
+        (tm.runFrom cfg τ).inputPos = 1 ∧
+        (tm.runFrom cfg τ).output = cfg.output ∧
+        tm.spaceUsed cfg τ ≤ s
+
+/-- A `TransformsTapes` statement can be read with a stronger precondition, a weaker postcondition
+and larger bounds. -/
+theorem TransformsTapes.imp {tm : MultiTapeTM k Symbol State}
+    {P P' : (input : List Symbol) → (Fin k → List Symbol) → Prop}
+    {Q Q' : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop}
+    {t s t' s' : ℕ} (h : TransformsTapes tm P Q t s)
+    (hP : ∀ input ws, P' input ws → P input ws)
+    (hQ : ∀ input ws ws', P' input ws → Q input ws ws' → Q' input ws ws')
+    (ht : t ≤ t') (hs : s ≤ s') :
+    TransformsTapes tm P' Q' t' s' := by
+  intro input ws cfg hstate hpos hholds hP'
+  obtain ⟨τ, hτ, ws', hhalt, hQ', hholds', hpos', hout, hspace⟩ :=
+    h input ws cfg hstate hpos hholds (hP input ws hP')
+  exact ⟨τ, hτ.trans ht, ws', hhalt, hQ input ws ws' hP' hQ', hholds', hpos', hout,
+    hspace.trans hs⟩
+
+/-- **Sequential composition.** `seq tm₁ tm₂` performs the transformation of `tm₁` and then the one
+of `tm₂`, provided the postcondition of `tm₁` implies the precondition of `tm₂`. -/
+theorem transformsTapes_seq {State₁ State₂ : Type*}
+    {tm₁ : MultiTapeTM k Symbol State₁} {tm₂ : MultiTapeTM k Symbol State₂}
+    {P₁ P₂ : (input : List Symbol) → (Fin k → List Symbol) → Prop}
+    {Q₁ Q₂ : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop}
+    {t₁ s₁ t₂ s₂ : ℕ}
+    (h₁ : TransformsTapes tm₁ P₁ Q₁ t₁ s₁) (h₂ : TransformsTapes tm₂ P₂ Q₂ t₂ s₂)
+    (hmid : ∀ input ws ws', P₁ input ws → Q₁ input ws ws' → P₂ input ws') :
+    TransformsTapes (tm₁.seq tm₂) P₁
+      (fun input ws ws'' => ∃ ws', Q₁ input ws ws' ∧ Q₂ input ws' ws'') (t₁ + t₂) (s₁ + s₂) :=
+  sorry
+
+/-- **The machine that does nothing.** It halts in one step, leaving every tape as it was. -/
+theorem exists_transformsTapes_nop (k : ℕ) :
+    ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State),
+      TransformsTapes tm (fun _ _ => True) (fun _ ws ws' => ws' = ws) 1 k :=
+  sorry
+
+/-- **Clearing a tape.** A work tape can be blanked and rewound in time linear in its contents,
+leaving all other tapes untouched: the result is exactly the old vector of words with tape `i`
+blanked. -/
+theorem exists_transformsTapes_clear {k : ℕ} (i : Fin k) :
+    ∃ (c : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ w : List Bool,
+      TransformsTapes tm (fun _ ws => ws i = w)
+        (fun _ ws ws' => ws' = Function.update ws i [])
+        (c * (w.length + 1)) (w.length + 1 + k) :=
+  sorry
+
+/-- **Branching on the first symbol of a tape.** Two machines performing transformations with the
+same postcondition can be combined into a machine that behaves like the first one if tape `i`
+starts with the symbol `x`, and like the second one otherwise. One step is spent reading the
+symbol.
+
+The specifications are families over an arbitrary index type, since a single machine has to be
+specified once for every value its bounds depend on. -/
+theorem exists_transformsTapes_branch {J : Type*} {k : ℕ} (i : Fin k) (x : Bool)
+    {State₁ State₂ : Type} [Finite State₁] [Finite State₂]
+    {tm₁ : MultiTapeTM k Bool State₁} {tm₂ : MultiTapeTM k Bool State₂}
+    {P₁ P₂ : J → (input : List Bool) → (Fin k → List Bool) → Prop}
+    {Q : J → (input : List Bool) → (Fin k → List Bool) → (Fin k → List Bool) → Prop}
+    {t₁ s₁ t₂ s₂ : J → ℕ}
+    (h₁ : ∀ j, TransformsTapes tm₁ (P₁ j) (Q j) (t₁ j) (s₁ j))
+    (h₂ : ∀ j, TransformsTapes tm₂ (P₂ j) (Q j) (t₂ j) (s₂ j)) :
+    ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ j : J,
+      TransformsTapes tm
+        (fun input ws => if (ws i).head? = some x then P₁ j input ws else P₂ j input ws)
+        (Q j) (max (t₁ j) (t₂ j) + 1) (max (s₁ j) (s₂ j) + k) :=
+  sorry
+
+/-- **Repeating a machine.** `tm` is run over and over; after each run the first symbol of tape `i`
+is inspected, and the machine halts as soon as it is `x`. This is the loop-back that `seq` cannot
+express: `seq` sends the halting state of one machine to the initial state of the *next* one,
+whereas here it is sent back to the initial state of the *same* one.
+
+The loop is specified by an invariant `P j n` holding at the start of round `n`: rounds
+`0, …, N j - 1` re-establish the invariant and leave the flag unset, and round `N j` establishes
+the postcondition `R j` and sets the flag. Each round costs at most `t j` steps, plus one step for
+the inspection.
+
+The space bound is `2 * k * s j + k` rather than `s j`: a round starts with all heads at `0` and
+heads move by at most one cell per step, so the cells it visits form an interval around `0` of
+length at most `s j`; the cells visited by *all* rounds therefore lie within distance `s j` of `0`
+on each of the `k` tapes. -/
+theorem exists_transformsTapes_repeat {J : Type*} {k : ℕ} (i : Fin k) (x : Bool)
+    {State₀ : Type} [Finite State₀] {tm : MultiTapeTM k Bool State₀}
+    {P : J → ℕ → (input : List Bool) → (Fin k → List Bool) → Prop}
+    {R : J → (input : List Bool) → (Fin k → List Bool) → Prop}
+    {N : J → ℕ} {t s : J → ℕ}
+    (hround : ∀ (j : J) (n : ℕ), n < N j → TransformsTapes tm (P j n)
+      (fun input _ ws' => P j (n + 1) input ws' ∧ (ws' i).head? ≠ some x) (t j) (s j))
+    (hstop : ∀ j : J, TransformsTapes tm (P j (N j))
+      (fun input _ ws' => R j input ws' ∧ (ws' i).head? = some x) (t j) (s j)) :
+    ∃ (State : Type) (_ : Finite State) (tm' : MultiTapeTM k Bool State), ∀ j : J,
+      TransformsTapes tm' (P j 0) (fun input _ ws' => R j input ws')
+        ((N j + 1) * (t j + 1)) (2 * k * s j + k) :=
+  sorry
+
+/-- **Evaluating a computable function on work tapes.** A function computable in time `t` and space
+`s` can be evaluated inside any machine that has enough work tapes: it reads its argument from tape
+`i`, writes its result to tape `o`, and uses `m` further tapes as scratch space. The tapes in
+`keep` are left untouched, all other tapes are blank before and after.
+
+Under the precondition — the argument on tape `i`, everything outside `keep` blank — the machine
+changes exactly one word: tape `i` and the tapes in `keep` are untouched and the scratch tapes are
+blank again, so the postcondition is the single equality `ws' = Function.update ws o …`.
+
+The length of the argument and of the result enter the bounds because they are written to and read
+from work tapes; neither is bounded by `t` or `s`, since the input tape is read-only and the output
+tape is append-only. -/
+theorem exists_transformsTapes_ofComputable {α β : Type*} {enc : α ↪ List Bool}
+    {encOut : β ↪ List Bool} {g : α → β} {t s : α → ℕ}
+    (h : ComputableInTimeAndSpace g enc encOut t s) :
+    ∃ m c : ℕ, ∀ (k : ℕ) (i o : Fin k) (keep : Finset (Fin k)),
+      i ≠ o → i ∉ keep → o ∉ keep → m + 2 + keep.card ≤ k →
+      ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ a : α,
+        TransformsTapes tm
+          (fun _ ws => ws i = enc a ∧ ∀ l, l ≠ i → l ∉ keep → ws l = [])
+          (fun _ ws ws' => ws' = Function.update ws o (encOut (g a)))
+          (c * (t a + (enc a).length + (encOut (g a)).length + 1))
+          (c * (s a + (enc a).length + (encOut (g a)).length + 1) + k) :=
+  sorry
+
+/-- **Evaluating a computable function on the input.** Like
+`exists_transformsTapes_ofComputable`, except that the argument is read from the real input tape,
+so it does not have to be copied onto a work tape first and its length does not enter the space
+bound. -/
+theorem exists_transformsTapes_ofComputableInput {α β : Type*} {enc : α ↪ List Bool}
+    {encOut : β ↪ List Bool} {g : α → β} {t s : α → ℕ}
+    (h : ComputableInTimeAndSpace g enc encOut t s) :
+    ∃ m c : ℕ, ∀ (k : ℕ) (o : Fin k) (keep : Finset (Fin k)),
+      o ∉ keep → m + 1 + keep.card ≤ k →
+      ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ a : α,
+        TransformsTapes tm
+          (fun input ws => input = enc a ∧ ∀ l, l ∉ keep → ws l = [])
+          (fun _ ws ws' => ws' = Function.update ws o (encOut (g a)))
+          (c * (t a + (encOut (g a)).length + 1))
+          (c * (s a + (encOut (g a)).length + 1) + k) :=
+  sorry
+
+/-- **From a tape transformation back to a computation.** A machine that, started on blank work
+tapes with the input tape holding `encIn a`, halts with tape `o` holding `encOut (g a)`, computes
+`g` once the contents of `o` are emitted as the output. -/
+theorem computableInTimeAndSpace_of_transformsTapes {α β : Type*} {k : ℕ} (o : Fin k)
+    {State : Type} [Finite State] {tm : MultiTapeTM k Bool State}
+    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {g : α → β} {t s : α → ℕ}
+    (h : ∀ a : α, TransformsTapes tm
+      (fun input ws => input = encIn a ∧ ∀ l, ws l = [])
+      (fun _ _ ws' => ws' o = encOut (g a)) (t a) (s a)) :
+    ∃ c, ComputableInTimeAndSpace g encIn encOut
+      (fun a => c * (t a + (encOut (g a)).length + 1))
+      (fun a => c * (s a + (encOut (g a)).length + 1)) :=
+  sorry
+
+end Turing.MultiTapeTM
diff --git a/Cslib/Foundations/Semantics/LTS/Execution.lean b/Cslib/Foundations/Semantics/LTS/Execution.lean
index fd49f191e0..7479aa6e86 100644
--- a/Cslib/Foundations/Semantics/LTS/Execution.lean
+++ b/Cslib/Foundations/Semantics/LTS/Execution.lean
@@ -96,6 +96,8 @@ theorem mTr_iff_execution :
     lts.MTr s1 μs s2 ↔ ∃ ss : List State, lts.Execution s1 μs s2 ss := by
   grind
 
+-- Merging the `have` into `grind` triples this file's compile time.
+set_option linter.tacticAnalysis.mergeWithGrind false in
 private lemma Execution.comp_helper
     {lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State}
     (h1 : lts.Execution s μs1 r ss1) (h2 : lts.Execution r μs2 t ss2)
diff --git a/Cslib/Foundations/Semantics/LTS/MapHom.lean b/Cslib/Foundations/Semantics/LTS/MapHom.lean
index 95212a26cf..f1b2774ee3 100644
--- a/Cslib/Foundations/Semantics/LTS/MapHom.lean
+++ b/Cslib/Foundations/Semantics/LTS/MapHom.lean
@@ -48,8 +48,7 @@ theorem mapHom_mTr {lts : LTS State Label₁} {μs : List Label₂} :
   | cons μ μs ih =>
     rw [Hom.map_cons]
     apply Iff.intro .. <;> intro h
-    · obtain ⟨_, _, _⟩ := MTr.cons_iff.mp h
-      grind [mapHom_tr, MTr.append_iff (lts := lts)]
+    · grind [mapHom_tr, MTr.append_iff (lts := lts)]
     · obtain ⟨_, _, _⟩ := (MTr.append_iff (lts := lts)).mp h
       grind [mapHom_tr, MTr.cons_iff (lts := lts.mapHom f)]
 
diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean
index ae423a9aa6..0b251f1e13 100644
--- a/Cslib/Logics/HML/LogicalEquivalence.lean
+++ b/Cslib/Logics/HML/LogicalEquivalence.lean
@@ -99,8 +99,8 @@ instance (lts : LTS State Label) :
       intro s
       rw [Satisfies.iff_iff_iff]
       apply Iff.intro
-      all_goals
-        rintro ⟨w', h⟩
+      · grind [=_ Proposition.Context.fill_def]
+      · rintro ⟨w', h⟩
         specialize ih w'
         grind [=_ Proposition.Context.fill_def]
 
diff --git a/CslibTests.lean b/CslibTests.lean
index 94af0f1566..dbfb6976d0 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -2,6 +2,7 @@ import CslibTests.Bisimulation
 import CslibTests.CCS
 import CslibTests.CCS.VendingMachine
 import CslibTests.CLL
+import CslibTests.Complexity.Combinators
 import CslibTests.Congruence
 import CslibTests.DFA
 import CslibTests.FreeMonad
diff --git a/CslibTests/Complexity/Combinators.lean b/CslibTests/Complexity/Combinators.lean
new file mode 100644
index 0000000000..cdf05d75be
--- /dev/null
+++ b/CslibTests/Complexity/Combinators.lean
@@ -0,0 +1,558 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Tactic.FinCases
+import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp
+import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Ite
+import Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option
+import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Tuple
+
+namespace CslibTests
+
+open Cslib Turing MultiTapeTM
+
+/-- The Boolean `and` function is computable in constant time and zero space. -/
+example : ∀ encIn encOut, ∃ c, ComputableInTimeAndSpace
+    (encIn := encIn)
+    (encOut := encOut)
+    (Function.uncurry Bool.and)
+    (fun _ => c) (fun _ => 0) := by
+  intro encIn encOut
+  apply computableInTimeAndSpace_of_finite
+
+def fullAdder (a b carry : Bool) : Bool × Bool :=
+  let sum := (a != b) != carry
+  let newCarry := (a && b) || (carry && (a != b))
+  (sum, newCarry)
+
+/-- The binary full adder is computable in constant time and zero space. -/
+example : ∀ encIn encOut, ∃ c, ComputableInTimeAndSpace
+    (encIn := encIn)
+    (encOut := encOut)
+    (Function.uncurry fullAdder)
+    (fun _ => c) (fun _ => 0) := by
+  intro encIn encOut
+  apply computableInTimeAndSpace_of_finite
+
+/-- Equality comparison to a constant is computable in constant time and zero space,
+also for infinite domains. -/
+example {α : Type*} [DecidableEq α] : ∀ encIn encOut out, ∃ c, ComputableInTimeAndSpace
+    (encIn := encIn)
+    (encOut := encOut)
+    (fun a : α => a == out)
+    (fun _ => c) (fun _ => 0) := by
+  intro encIn encOut out
+  refine computableInTimeAndSpace_of_exists_finite_ne ⟨false, ?_⟩
+  exact Set.Finite.subset (Set.finite_singleton out) (by intro a ha; simp_all)
+
+/-! ## Case analysis
+
+The single primitive `computableInTimeAndSpace_match` covers all of them: it needs nothing of the
+scrutinee's type beyond being finite, and `cond`, `ite` and `dite` are its instances at `Bool`. -/
+
+/-- A conditional on a decidable predicate is computable as soon as the predicate is decided by a
+machine and both branches are computable. Only the branch that is taken runs, hence the `max`. -/
+example {α β : Type} {encIn : α ↪ List Bool} {encBool : Bool ↪ List Bool} {encOut : β ↪ List Bool}
+    {p : α → Prop} [DecidablePred p] {f g : α → β} {tc sc tf sf tg sg : α → ℕ}
+    (hp : ComputableInTimeAndSpace (fun a => decide (p a)) encIn encBool tc sc)
+    (hf : ComputableInTimeAndSpace f encIn encOut tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encOut tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun a => if p a then f a else g a) encIn encOut
+      (fun a => c * (tc a + max (tf a) (tg a) + 1))
+      (fun a => c * (sc a + max (sf a) (sg a) + 1)) :=
+  computableInTimeAndSpace_ite hp hf hg
+
+/-- A `match` on a finite inductive type is computable as soon as the scrutinee and every branch
+are — here on `Ordering`, the result of a `compare`. Nothing about the type is needed beyond
+`Finite`. The scrutinee and the branches share one pair of bounds, which costs nothing: separate
+bounds are weakened to a common one, as here where the scrutinee's and the branches' are added.
+Testing which constructor the scrutinee is costs no space beyond the scrutinee's own, since a
+finite type has only finitely many encodings and so the encoded scrutinee is of constant length. -/
+example {α β : Type} {encIn : α ↪ List Bool} {encO : Ordering ↪ List Bool}
+    {encOut : β ↪ List Bool}
+    {sel : α → Ordering} {onLt onEq onGt : α → β} {tsel ssel t s : α → ℕ}
+    (hsel : ComputableInTimeAndSpace sel encIn encO tsel ssel)
+    (hlt : ComputableInTimeAndSpace onLt encIn encOut t s)
+    (heq : ComputableInTimeAndSpace onEq encIn encOut t s)
+    (hgt : ComputableInTimeAndSpace onGt encIn encOut t s) :
+    ∃ c, ComputableInTimeAndSpace
+      (fun a => match sel a with
+        | .lt => onLt a
+        | .eq => onEq a
+        | .gt => onGt a)
+      encIn encOut
+      (fun a => c * (tsel a + t a + 1))
+      (fun a => c * (ssel a + s a + 1)) := by
+  have hweak : ∀ g : α → β, ComputableInTimeAndSpace g encIn encOut t s →
+      ComputableInTimeAndSpace g encIn encOut (fun a => tsel a + t a) (fun a => ssel a + s a) :=
+    fun _ h => h.mono (fun a => Nat.le_add_left _ _) (fun a => Nat.le_add_left _ _)
+  have hbr : ∀ i : Ordering, ComputableInTimeAndSpace
+      (fun a => match i with | .lt => onLt a | .eq => onEq a | .gt => onGt a)
+      encIn encOut (fun a => tsel a + t a) (fun a => ssel a + s a) := by
+    intro i
+    cases i
+    exacts [hweak _ hlt, hweak _ heq, hweak _ hgt]
+  exact computableInTimeAndSpace_match (Set.toFinite _) (fun _ => rfl)
+    (hsel.mono (fun a => Nat.le_add_right _ _) (fun a => Nat.le_add_right _ _)) fun i _ => hbr i
+
+/-- Branches of *different* result types need no dependent version of the combinator: the output
+type is the sigma, and the case analysis is the same theorem instantiated at it. What makes this
+work is that computability depends only on the encoded strings, not on the types they encode, so
+the eliminator's `motive` has no computational content. -/
+example {α ι : Type} [Finite ι] {β : ι → Type}
+    {sel : α → ι} {br : (i : ι) → α → β i}
+    {encIn : α ↪ List Bool} {encι : ι ↪ List Bool} {encS : (Σ i, β i) ↪ List Bool}
+    {t s : α → ℕ}
+    (hsel : ComputableInTimeAndSpace sel encIn encι t s)
+    (hbr : ∀ i, ComputableInTimeAndSpace (fun a => (⟨i, br i a⟩ : Σ i, β i)) encIn encS t s) :
+    ∃ c, ComputableInTimeAndSpace (fun a => (⟨sel a, br (sel a) a⟩ : Σ i, β i)) encIn encS
+      (fun a => c * (t a + 1)) (fun a => c * (s a + 1)) :=
+  computableInTimeAndSpace_match (br := fun i a => (⟨i, br i a⟩ : Σ i, β i))
+    (Set.toFinite _) (fun _ => rfl) hsel fun i _ => hbr i
+
+/-! ## Constructors
+
+Dually to the eliminator, a constructor of a non-recursive inductive type is the introduction rule
+of a finite product, so it is `computableInTimeAndSpace_concat` nested once per field. Unlike the
+eliminator, every field is computed, so the fields contribute their sum rather than their maximum;
+and unlike the eliminator, nothing is required of the encoding beyond that it be the concatenation
+of the encoded fields. -/
+
+/-- A two-field constructor carrying data from an infinite type. -/
+structure Interval where
+  lo : ℕ
+  hi : ℕ
+
+example {α : Type} {encIn : α ↪ List Bool} {encN : ℕ ↪ List Bool} {encI : Interval ↪ List Bool}
+    {lo hi : α → ℕ} {tl sl th sh : α → ℕ}
+    (henc : ∀ a, encI ⟨lo a, hi a⟩ = encN (lo a) ++ encN (hi a))
+    (hlo : ComputableInTimeAndSpace lo encIn encN tl sl)
+    (hhi : ComputableInTimeAndSpace hi encIn encN th sh) :
+    ∃ c, ComputableInTimeAndSpace (fun a => (⟨lo a, hi a⟩ : Interval)) encIn encI
+      (fun a => c * (tl a + th a + (encIn a).length + 1))
+      (fun a => c * (sl a + sh a + 1)) := by
+  exact computableInTimeAndSpace_ctor (A := fun _ : Fin 2 => ℕ) (fs := ![lo, hi])
+    (encIn := encIn) (encA := fun _ => encN)
+    (t := fun a => tl a + th a) (s := fun a => sl a + sh a)
+    (fun a => by simpa [List.ofFn_succ] using henc a)
+    (Fin.forall_fin_two.mpr
+      ⟨by simpa using hlo.mono (fun a => by omega) (fun a => by omega),
+        by simpa using hhi.mono (fun a => by omega) (fun a => by omega)⟩)
+
+/-- `Option.some`, at the canonical encoding of `Encodings.Option`. A tagged constructor is built
+by treating the tag as a field computed by a constant function, so nothing beyond
+`computableInTimeAndSpace_concat` is involved. -/
+example {α : Type} {enc : α ↪ List Bool} :
+    ∃ c, ComputableInTimeAndSpace (fun a => (some a : Option α)) enc (encOption enc)
+      (fun a => c * ((enc a).length + 1)) (fun _ => c) := by
+  obtain ⟨c₁, h₁⟩ := computableInTimeAndSpace_of_const (α := α) (encIn := enc)
+    (encOut := (⟨fun _ => [true], fun a b _ => Subsingleton.elim a b⟩ : Unit ↪ List Bool)) ()
+  obtain ⟨c₂, h₂⟩ := computableInTimeAndSpace_id (α := α) (enc := enc)
+  obtain ⟨c₃, h₃⟩ := computableInTimeAndSpace_concat (h := fun a => (some a : Option α))
+    (encD := encOption enc) (fun _ => rfl) h₁ h₂
+  refine ⟨c₁ + c₂ + c₃ + 3, h₃.mono (fun a => ?_) (fun a => by omega)⟩
+  have hexp : (c₁ + c₂ + c₃ + 3) * ((enc a).length + 1)
+      = c₁ * ((enc a).length + 1) + c₂ * ((enc a).length + 1) + c₃ * ((enc a).length + 1)
+        + 3 * ((enc a).length + 1) := by ring
+  have h1 : c₁ ≤ c₁ * ((enc a).length + 1) := Nat.le_mul_of_pos_right _ (by omega)
+  omega
+
+/-- A subtype constructor costs nothing at all: the proof field is erased, so the encoding of the
+constructed value *is* the encoding of the data field, and the whole constructor is a change of
+coordinates — `ComputableInTimeAndSpace.congr`, with no combinator involved. -/
+example {α β : Type} {p : β → Prop} {encIn : α ↪ List Bool} {encB : β ↪ List Bool}
+    {encS : {x // p x} ↪ List Bool} {f : α → β} {t s : α → ℕ}
+    (hp : ∀ a, p (f a)) (henc : ∀ x : {x // p x}, encS x = encB x.val)
+    (hf : ComputableInTimeAndSpace f encIn encB t s) :
+    ComputableInTimeAndSpace (fun a => (⟨f a, hp a⟩ : {x // p x})) encIn encS t s :=
+  hf.congr (fun _ => rfl) fun _ => henc _
+
+/-- Three fields of different types, encoded flat rather than as nested pairs. The index family of
+`computableInTimeAndSpace_ctor` is dependent, which is awkward when the fields have different
+types; the `List Bool`-valued `computableInTimeAndSpace_flatten` avoids it — encode each field,
+concatenate, and read the result back with `ComputableInTimeAndSpace.congr`. -/
+example {α : Type} {encIn : α ↪ List Bool} {encN : ℕ ↪ List Bool} {encB : Bool ↪ List Bool}
+    {encT : ℕ × Bool × ℕ ↪ List Bool} {f h : α → ℕ} {g : α → Bool} {t₁ s₁ t₂ s₂ t₃ s₃ : α → ℕ}
+    (henc : ∀ a, encT (f a, g a, h a) = encN (f a) ++ encB (g a) ++ encN (h a))
+    (hf : ComputableInTimeAndSpace f encIn encN t₁ s₁)
+    (hg : ComputableInTimeAndSpace g encIn encB t₂ s₂)
+    (hh : ComputableInTimeAndSpace h encIn encN t₃ s₃) :
+    ∃ c, ComputableInTimeAndSpace (fun a => (f a, g a, h a)) encIn encT
+      (fun a => c * (t₁ a + t₂ a + t₃ a + (encIn a).length + 1))
+      (fun a => c * (s₁ a + s₂ a + s₃ a + 1)) := by
+  obtain ⟨c, hc⟩ := computableInTimeAndSpace_flatten (encIn := encIn)
+    (fs := ![fun a => encN (f a), fun a => encB (g a), fun a => encN (h a)])
+    (t := fun a => t₁ a + t₂ a + t₃ a) (s := fun a => s₁ a + s₂ a + s₃ a)
+    (by
+      intro j
+      fin_cases j
+      · exact (hf.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega)
+      · exact (hg.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega)
+      · exact (hh.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega))
+  exact ⟨c, hc.congr (fun _ => rfl) (fun a => by simpa [List.ofFn_succ] using henc a)⟩
+
+/-! ## A proper inductive type
+
+`Shape` has several alternatives of different arities, two of them carrying data from an infinite
+type. Its constructors are covered by the combinators below; its eliminator is covered as far as
+the tag, and no further — see the last example. -/
+
+/-- Three alternatives, of arities zero, one and two. -/
+inductive Shape
+  | point
+  | circle (r : ℕ)
+  | rect (w h : ℕ)
+deriving DecidableEq
+
+/-- Which alternative a shape is. -/
+def Shape.tag : Shape → Fin 3
+  | .point => 0
+  | .circle _ => 1
+  | .rect _ _ => 2
+
+section Shape
+
+variable {α : Type} {encIn : α ↪ List Bool} {encN : ℕ ↪ List Bool} {encS : Shape ↪ List Bool}
+
+/-- A nullary constructor is a constant, so it needs nothing at all of the encoding. -/
+example : ∃ c, ComputableInTimeAndSpace (fun _ : α => Shape.point) encIn encS
+    (fun _ => c) (fun _ => 0) :=
+  computableInTimeAndSpace_of_const _
+
+/-- A constructor with one field. The two-bit tag is a field computed by a constant function, so
+this is one `computableInTimeAndSpace_concat` and nothing else. -/
+example {f : α → ℕ} {t s : α → ℕ}
+    (henc : ∀ r, encS (.circle r) = [false, true] ++ encN r)
+    (hf : ComputableInTimeAndSpace f encIn encN t s) :
+    ∃ c, ComputableInTimeAndSpace (fun a => Shape.circle (f a)) encIn encS
+      (fun a => c * (t a + (encIn a).length + 1)) (fun a => c * (s a + 1)) := by
+  obtain ⟨c₁, h₁⟩ := computableInTimeAndSpace_of_const (α := α) (encIn := encIn)
+    (encOut := (⟨fun _ => [false, true], fun a b _ => Subsingleton.elim a b⟩ : Unit ↪ List Bool)) ()
+  obtain ⟨c₂, h₂⟩ := computableInTimeAndSpace_concat (h := fun a => Shape.circle (f a))
+    (encD := encS) (fun a => henc (f a)) h₁ hf
+  refine ⟨c₁ + c₂ + 3, h₂.mono (fun a => ?_) (fun a => ?_)⟩
+  · have hexp : (c₁ + c₂ + 3) * (t a + (encIn a).length + 1)
+        = c₁ * (t a + (encIn a).length + 1) + c₂ * (t a + (encIn a).length + 1)
+          + 3 * (t a + (encIn a).length + 1) := by ring
+    have h1 : c₁ ≤ c₁ * (t a + (encIn a).length + 1) := Nat.le_mul_of_pos_right _ (by omega)
+    omega
+  · have hexp : (c₁ + c₂ + 3) * (s a + 1)
+        = c₁ * (s a + 1) + c₂ * (s a + 1) + 3 * (s a + 1) := by ring
+    have h2 : c₂ ≤ c₂ * (s a + 1) := Nat.le_mul_of_pos_right _ (by omega)
+    omega
+
+/-- A constructor with two fields: the tag and the two fields are three computations whose outputs
+are concatenated, so `computableInTimeAndSpace_flatten` applies directly and there is no need to
+nest pairs. -/
+example {f g : α → ℕ} {tf sf tg sg : α → ℕ}
+    (henc : ∀ w h, encS (.rect w h) = [true, false] ++ encN w ++ encN h)
+    (hf : ComputableInTimeAndSpace f encIn encN tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encN tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun a => Shape.rect (f a) (g a)) encIn encS
+      (fun a => c * (tf a + tg a + (encIn a).length + 1))
+      (fun a => c * (sf a + sg a + 1)) := by
+  obtain ⟨c₀, h₀⟩ := computableInTimeAndSpace_of_const (α := α) (encIn := encIn)
+    (encOut := Function.Embedding.refl (List Bool)) ([true, false] : List Bool)
+  obtain ⟨c, hc⟩ := computableInTimeAndSpace_flatten (encIn := encIn)
+    (fs := ![fun _ => [true, false], fun a => encN (f a), fun a => encN (g a)])
+    (t := fun a => c₀ + tf a + tg a) (s := fun a => sf a + sg a)
+    (by
+      intro j
+      fin_cases j
+      · exact h₀.mono (fun a => by omega) (fun a => by omega)
+      · exact (hf.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega)
+      · exact (hg.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega))
+  refine ⟨c * (c₀ + 1), ((hc.congr (fun _ => rfl)
+    (fun a => by simpa [List.ofFn_succ] using henc (f a) (g a))).mono (fun a => ?_)
+      (fun a => ?_))⟩
+  · calc c * (c₀ + tf a + tg a + (encIn a).length + 1)
+        ≤ c * ((c₀ + 1) * (tf a + tg a + (encIn a).length + 1)) := by
+          refine Nat.mul_le_mul_left _ ?_
+          have h1 : c₀ ≤ c₀ * (tf a + tg a + (encIn a).length + 1) :=
+            Nat.le_mul_of_pos_right _ (by omega)
+          have h2 : (c₀ + 1) * (tf a + tg a + (encIn a).length + 1)
+              = c₀ * (tf a + tg a + (encIn a).length + 1)
+                + (tf a + tg a + (encIn a).length + 1) := by ring
+          omega
+      _ = c * (c₀ + 1) * (tf a + tg a + (encIn a).length + 1) := by ring
+  · exact Nat.mul_le_mul_right _ (Nat.le_mul_of_pos_right _ (by omega))
+
+/-- Matching on a type with several alternatives, as far as the tag. Given that the alternative can
+be read off — which is a requirement on the encoding, not something derivable, and the one piece
+`Encodings/` would have to supply for a general type — the `match` is
+`computableInTimeAndSpace_match` at the tag.
+
+Branches that *use* a constructor's fields need more: a computable destructor per constructor, and
+pairing to hand the branch both the original input and the extracted payload. Those are the two
+things still missing, and they are requirements on the encoding rather than combinators. -/
+example {β : Type} {encF : Fin 3 ↪ List Bool} {encOut : β ↪ List Bool}
+    {sel : α → Shape} {onPoint onCircle onRect : α → β} {tsel ssel t s : α → ℕ}
+    (htag : ComputableInTimeAndSpace (fun a => (sel a).tag) encIn encF tsel ssel)
+    (hp : ComputableInTimeAndSpace onPoint encIn encOut t s)
+    (hc : ComputableInTimeAndSpace onCircle encIn encOut t s)
+    (hr : ComputableInTimeAndSpace onRect encIn encOut t s) :
+    ∃ c, ComputableInTimeAndSpace
+      (fun a => match sel a with
+        | .point => onPoint a
+        | .circle _ => onCircle a
+        | .rect _ _ => onRect a)
+      encIn encOut
+      (fun a => c * (tsel a + t a + 1)) (fun a => c * (ssel a + s a + 1)) := by
+  have hweak : ∀ g : α → β, ComputableInTimeAndSpace g encIn encOut t s →
+      ComputableInTimeAndSpace g encIn encOut (fun a => tsel a + t a) (fun a => ssel a + s a) :=
+    fun _ h => h.mono (fun a => Nat.le_add_left _ _) (fun a => Nat.le_add_left _ _)
+  have hbr : ∀ i : Fin 3, ComputableInTimeAndSpace (![onPoint, onCircle, onRect] i)
+      encIn encOut (fun a => tsel a + t a) (fun a => ssel a + s a) := by
+    intro i
+    fin_cases i
+    · exact hweak _ hp
+    · exact hweak _ hc
+    · exact hweak _ hr
+  exact computableInTimeAndSpace_match (Set.toFinite _) (fun a => by cases sel a <;> rfl)
+    (htag.mono (fun a => Nat.le_add_right _ _) (fun a => Nat.le_add_right _ _)) fun i _ => hbr i
+
+/-- The payload of `circle`, and of anything else by convention. -/
+def Shape.r : Shape → ℕ
+  | .circle r => r
+  | _ => 0
+
+/-- The first payload of `rect`, and of anything else by convention. -/
+def Shape.w : Shape → ℕ
+  | .rect w _ => w
+  | _ => 0
+
+/-- The second payload of `rect`, and of anything else by convention. -/
+def Shape.h : Shape → ℕ
+  | .rect _ h => h
+  | _ => 0
+
+/-- **A destructuring `match` whose branches need junk.** `Span`'s alternatives all have arity two,
+so its fields are total functions and nothing is invented. `Shape`'s have arities zero, one and
+two, so `Shape.r` has to return something on a `rect` and `Shape.w` on a `circle`, and the value
+chosen — `0` here — is arbitrary.
+
+That is exactly what `hagree` licenses. The `circle` branch reads `Shape.w`'s junk nowhere, because
+it is only ever run where the scrutinee is a `circle`, and the hypothesis only asks the branches to
+agree with the `match` where they are taken. A version of the combinator demanding the branches
+equal the `match` everywhere could not be applied here at all: off its own alternative each branch
+computes something the `match` never returns.
+
+Note the branch family is written `fun a => ![…] i` and not `![…] i` with the input abstracted
+inside each entry. The two are equal by `funext`, but only in the first does the scrutinee occur
+applied to the outer variable, and `cases` cannot generalise it under a binder — with the other
+spelling `hagree` is no longer `rfl`. -/
+example {β : Type} {encF : Fin 3 ↪ List Bool} {encOut : β ↪ List Bool}
+    {sel : α → Shape} {onPoint : α → β} {onCircle : α → ℕ → β} {onRect : α → ℕ → ℕ → β}
+    {t s : α → ℕ}
+    (htag : ComputableInTimeAndSpace (fun a => (sel a).tag) encIn encF t s)
+    (hbr : ∀ i : Fin 3, ComputableInTimeAndSpace
+      (fun a => ![onPoint a, onCircle a (sel a).r, onRect a (sel a).w (sel a).h] i)
+      encIn encOut t s) :
+    ∃ c, ComputableInTimeAndSpace
+      (fun a => match sel a with
+        | .point => onPoint a
+        | .circle r => onCircle a r
+        | .rect w h => onRect a w h)
+      encIn encOut
+      (fun a => c * (t a + 1)) (fun a => c * (s a + 1)) :=
+  computableInTimeAndSpace_match (Set.toFinite _) (fun a => by cases sel a <;> rfl) htag
+    fun i _ => hbr i
+
+end Shape
+
+/-! ## Several alternatives of the same arity
+
+`Shape` has only one constructor of arity two. `Span` has two, which is the case where the tag is
+doing real work: the two alternatives are indistinguishable by their payload and only the tag tells
+them apart. Each is built the same way — the tag and the two fields are three computations whose
+outputs are concatenated — so the construction is shared and only the tag and the constructor
+differ. -/
+
+/-- Two alternatives, each carrying two fields. -/
+inductive Span
+  | ofLength (start len : ℕ)
+  | ofBounds (lo hi : ℕ)
+deriving DecidableEq
+
+/-- Either alternative of `Span`, built from the tag and the two fields. -/
+private theorem span_ctor {α : Type} {encIn : α ↪ List Bool} {encN : ℕ ↪ List Bool}
+    {encS : Span ↪ List Bool} {f g : α → ℕ} {tf sf tg sg : α → ℕ}
+    (tag : List Bool) (mk : ℕ → ℕ → Span)
+    (henc : ∀ u v, encS (mk u v) = tag ++ encN u ++ encN v)
+    (hf : ComputableInTimeAndSpace f encIn encN tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encN tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun a => mk (f a) (g a)) encIn encS
+      (fun a => c * (tf a + tg a + (encIn a).length + 1))
+      (fun a => c * (sf a + sg a + 1)) := by
+  obtain ⟨c₀, h₀⟩ := computableInTimeAndSpace_of_const (α := α) (encIn := encIn)
+    (encOut := Function.Embedding.refl (List Bool)) tag
+  obtain ⟨c, hc⟩ := computableInTimeAndSpace_flatten (encIn := encIn)
+    (fs := ![fun _ => tag, fun a => encN (f a), fun a => encN (g a)])
+    (t := fun a => c₀ + tf a + tg a) (s := fun a => sf a + sg a)
+    (by
+      intro j
+      fin_cases j
+      · exact h₀.mono (fun a => by omega) (fun a => by omega)
+      · exact (hf.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega)
+      · exact (hg.congr (fun _ => rfl) fun _ => rfl).mono (fun a => by omega) (fun a => by omega))
+  refine ⟨c * (c₀ + 1), ((hc.congr (fun _ => rfl)
+    (fun a => by simpa [List.ofFn_succ] using henc (f a) (g a))).mono (fun a => ?_)
+      (fun a => ?_))⟩
+  · calc c * (c₀ + tf a + tg a + (encIn a).length + 1)
+        ≤ c * ((c₀ + 1) * (tf a + tg a + (encIn a).length + 1)) := by
+          refine Nat.mul_le_mul_left _ ?_
+          have h1 : c₀ ≤ c₀ * (tf a + tg a + (encIn a).length + 1) :=
+            Nat.le_mul_of_pos_right _ (by omega)
+          have h2 : (c₀ + 1) * (tf a + tg a + (encIn a).length + 1)
+              = c₀ * (tf a + tg a + (encIn a).length + 1)
+                + (tf a + tg a + (encIn a).length + 1) := by ring
+          omega
+      _ = c * (c₀ + 1) * (tf a + tg a + (encIn a).length + 1) := by ring
+  · exact Nat.mul_le_mul_right _ (Nat.le_mul_of_pos_right _ (by omega))
+
+/-- A function into a type with two two-field alternatives, choosing between them. The case
+analysis picks the constructor and each branch builds one, so this is `computableInTimeAndSpace_ite`
+over two instances of the constructor pattern; only the branch that is taken is built, hence the
+single copy of the field bounds. -/
+example {α : Type} {encIn : α ↪ List Bool} {encN : ℕ ↪ List Bool} {encS : Span ↪ List Bool}
+    {encBool : Bool ↪ List Bool} {sel : α → Bool} {f g : α → ℕ} {tc sc tf sf tg sg : α → ℕ}
+    (hlen : ∀ u v, encS (.ofLength u v) = [false] ++ encN u ++ encN v)
+    (hbnd : ∀ u v, encS (.ofBounds u v) = [true] ++ encN u ++ encN v)
+    (hsel : ComputableInTimeAndSpace sel encIn encBool tc sc)
+    (hf : ComputableInTimeAndSpace f encIn encN tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encN tg sg) :
+    ∃ c, ComputableInTimeAndSpace
+      (fun a => if sel a then Span.ofLength (f a) (g a) else Span.ofBounds (f a) (g a))
+      encIn encS
+      (fun a => c * (tc a + tf a + tg a + (encIn a).length + 1))
+      (fun a => c * (sc a + sf a + sg a + 1)) := by
+  obtain ⟨c₁, h₁⟩ := span_ctor [false] Span.ofLength hlen hf hg
+  obtain ⟨c₂, h₂⟩ := span_ctor [true] Span.ofBounds hbnd hf hg
+  obtain ⟨c₃, h₃⟩ := computableInTimeAndSpace_cond hsel h₁ h₂
+  refine ⟨c₃ * (c₁ + c₂ + 2), h₃.mono (fun a => ?_) (fun a => ?_)⟩
+  · have hmax : max (c₁ * (tf a + tg a + (encIn a).length + 1))
+          (c₂ * (tf a + tg a + (encIn a).length + 1))
+        ≤ (c₁ + c₂) * (tc a + tf a + tg a + (encIn a).length + 1) := by
+      have e : (c₁ + c₂) * (tc a + tf a + tg a + (encIn a).length + 1)
+          = c₁ * (tc a + tf a + tg a + (encIn a).length + 1)
+            + c₂ * (tc a + tf a + tg a + (encIn a).length + 1) := by ring
+      have e₁ : c₁ * (tf a + tg a + (encIn a).length + 1)
+          ≤ c₁ * (tc a + tf a + tg a + (encIn a).length + 1) := Nat.mul_le_mul_left _ (by omega)
+      have e₂ : c₂ * (tf a + tg a + (encIn a).length + 1)
+          ≤ c₂ * (tc a + tf a + tg a + (encIn a).length + 1) := Nat.mul_le_mul_left _ (by omega)
+      omega
+    calc c₃ * (tc a + max (c₁ * (tf a + tg a + (encIn a).length + 1))
+            (c₂ * (tf a + tg a + (encIn a).length + 1)) + 1)
+        ≤ c₃ * ((c₁ + c₂ + 2) * (tc a + tf a + tg a + (encIn a).length + 1)) := by
+          refine Nat.mul_le_mul_left _ ?_
+          have e : (c₁ + c₂ + 2) * (tc a + tf a + tg a + (encIn a).length + 1)
+              = (c₁ + c₂) * (tc a + tf a + tg a + (encIn a).length + 1)
+                + 2 * (tc a + tf a + tg a + (encIn a).length + 1) := by ring
+          omega
+      _ = c₃ * (c₁ + c₂ + 2) * (tc a + tf a + tg a + (encIn a).length + 1) := by ring
+  · have hmax : max (c₁ * (sf a + sg a + 1)) (c₂ * (sf a + sg a + 1))
+        ≤ (c₁ + c₂) * (sc a + sf a + sg a + 1) := by
+      have e : (c₁ + c₂) * (sc a + sf a + sg a + 1)
+          = c₁ * (sc a + sf a + sg a + 1) + c₂ * (sc a + sf a + sg a + 1) := by ring
+      have e₁ : c₁ * (sf a + sg a + 1) ≤ c₁ * (sc a + sf a + sg a + 1) :=
+        Nat.mul_le_mul_left _ (by omega)
+      have e₂ : c₂ * (sf a + sg a + 1) ≤ c₂ * (sc a + sf a + sg a + 1) :=
+        Nat.mul_le_mul_left _ (by omega)
+      omega
+    calc c₃ * (sc a + max (c₁ * (sf a + sg a + 1)) (c₂ * (sf a + sg a + 1)) + 1)
+        ≤ c₃ * ((c₁ + c₂ + 2) * (sc a + sf a + sg a + 1)) := by
+          refine Nat.mul_le_mul_left _ ?_
+          have e : (c₁ + c₂ + 2) * (sc a + sf a + sg a + 1)
+              = (c₁ + c₂) * (sc a + sf a + sg a + 1)
+                + 2 * (sc a + sf a + sg a + 1) := by ring
+          omega
+      _ = c₃ * (c₁ + c₂ + 2) * (sc a + sf a + sg a + 1) := by ring
+
+/-- Which alternative a span is. -/
+def Span.tag : Span → Bool
+  | .ofLength .. => false
+  | .ofBounds .. => true
+
+/-- The first field of either alternative. Total, because *both* alternatives carry two naturals,
+which is what makes a destructuring `match` on `Span` expressible without any junk: a branch may
+read the fields of the alternative it is not in, since it is never run there — but here it does
+not even have to. -/
+def Span.fst : Span → ℕ
+  | .ofLength u _ => u
+  | .ofBounds u _ => u
+
+/-- The second field of either alternative. -/
+def Span.snd : Span → ℕ
+  | .ofLength _ v => v
+  | .ofBounds _ v => v
+
+/-- **The eliminator of a type with two alternatives of arity two, destructuring.** The branches
+here do not ignore the payload as they do for `Shape`: each receives both fields of the alternative
+it matched, which is the case the combinator was supposed to cover and had not been checked on.
+
+It goes through unchanged. The branch family is indexed by the tag and each branch is the total
+function reading both fields, so `hagree` is the whole content of the destructuring, and it is
+`rfl` once the scrutinee is case split — the projections agree with the pattern variables by
+definition of the projections.
+
+The scrutinee is the input itself, so this is `Span`'s eliminator and nothing more; matching on a
+scrutinee *computed* from some other input is the same theorem with `sel` in front, as in the
+`Shape` examples.
+
+The two hypotheses are the whole of what a type has to supply. `htag` says the alternative can be
+read off, which is a requirement on `encS` and the one thing no combinator can provide. `hbr` says
+a branch is computable as a function of the value being matched rather than of its payload, and
+that is a computable destructor per field composed with the branch — pairing the two fields, since
+the branch is binary. Both are requirements on the encoding, not further combinators. -/
+example {β : Type} {encS : Span ↪ List Bool} {encB : Bool ↪ List Bool} {encOut : β ↪ List Bool}
+    {onLength onBounds : ℕ → ℕ → β} {t s : Span → ℕ}
+    (htag : ComputableInTimeAndSpace Span.tag encS encB t s)
+    (hbr : ∀ b : Bool, ComputableInTimeAndSpace
+      (fun x => (bif b then onBounds else onLength) x.fst x.snd) encS encOut t s) :
+    ∃ c, ComputableInTimeAndSpace
+      (fun x => match x with
+        | .ofLength u v => onLength u v
+        | .ofBounds u v => onBounds u v)
+      encS encOut
+      (fun x => c * (t x + 1)) (fun x => c * (s x + 1)) :=
+  computableInTimeAndSpace_match (Set.toFinite _) (fun x => by cases x <;> rfl) htag
+    fun b _ => hbr b
+
+/-- **The selector Lean already provides.** `Span.tag` above was written by hand, but every
+inductive type comes with `ctorIdx`, generated from `casesOn`, which is the same map read into `ℕ`.
+It serves as the scrutinee directly. That is what makes the combinator mechanisable: a tactic
+cannot invent a bespoke tag type for an arbitrary inductive, but `ctorIdx` is always there, and the
+side conditions — that its range is finite, and that the branches agree — are both discharged by
+case analysis on the scrutinee.
+
+The price of landing in `ℕ` is that the branch family is indexed by `ℕ` too, so all but two of its
+members are junk. That is why only the branches in the range of the selector are asked to be
+computable; over all of `ℕ` the hypothesis would be unsatisfiable for any nonconstant bound. -/
+example {β : Type} {encS : Span ↪ List Bool} {encN : ℕ ↪ List Bool} {encOut : β ↪ List Bool}
+    {onLength onBounds : ℕ → ℕ → β} {t s : Span → ℕ}
+    (hidx : ComputableInTimeAndSpace Span.ctorIdx encS encN t s)
+    (h₀ : ComputableInTimeAndSpace (fun x : Span => onLength x.fst x.snd) encS encOut t s)
+    (h₁ : ComputableInTimeAndSpace (fun x : Span => onBounds x.fst x.snd) encS encOut t s) :
+    ∃ c, ComputableInTimeAndSpace
+      (fun x => match x with
+        | .ofLength u v => onLength u v
+        | .ofBounds u v => onBounds u v)
+      encS encOut
+      (fun x => c * (t x + 1)) (fun x => c * (s x + 1)) := by
+  refine computableInTimeAndSpace_match
+    (br := fun i x => bif i == 0 then onLength x.fst x.snd else onBounds x.fst x.snd)
+    (((Set.finite_singleton 1).insert 0).subset ?_) (fun x => by cases x <;> rfl) hidx ?_
+  · rintro _ ⟨x, rfl⟩
+    cases x
+    · exact Set.mem_insert _ _
+    · exact Set.mem_insert_of_mem _ rfl
+  · rintro _ ⟨x, rfl⟩
+    cases x
+    · exact h₀
+    · exact h₁
+
+end CslibTests
diff --git a/lake-manifest.json b/lake-manifest.json
index 6e872d1b5a..381f3888fc 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0fa18d49e3c34d2b7766fe0cb6016e3bd68cd15a",
+   "rev": "e06eff5f95374108acfaf19f1ff7473aa7771df2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "0fa18d49e3c34d2b7766fe0cb6016e3bd68cd15a",
+   "inputRev": "e06eff5f95374108acfaf19f1ff7473aa7771df2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d54dddc581e08be364c278052863524bff7a99a9",
+   "rev": "7e23602c91bc04586b2b06de2708a041853e4681",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index b99041ff25..7e4e4eb3b0 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "0fa18d49e3c34d2b7766fe0cb6016e3bd68cd15a"
+rev = "e06eff5f95374108acfaf19f1ff7473aa7771df2"
 
 [[lean_lib]]
 name = "Cslib"