diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean
index 292d05d431..09e06559bb 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean
@@ -305,7 +305,7 @@ public theorem stepTime_iterate_le (x : List ℕ) (j : ℕ) :
   have hbits := ComputableTidilyInO.length_encNat_mono
     (show cfg.inputPos ≤ (encList encUnary x).length + 1 by omega)
   unfold stepTime stepBound
-  dsimp only
+  dsimp only [Ctx.desc, Ctx.input, Ctx.cfg]
   exact Nat.add_le_add
     (Nat.mul_le_mul (Nat.mul_le_mul_right _ (by omega)) (by omega))
     (Nat.mul_le_mul (by omega) (by gcongr))
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean
index 0d96f32218..8263a2401a 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean
@@ -18,6 +18,7 @@ import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists
 
 /-!
 # The cost of a step of the simulation
@@ -26,7 +27,8 @@ States, symbols and moves are encoded in unary (`Turing.MultiTapeTM.encUnary`),
 the work tapes as integers (`Turing.MultiTapeTM.encInt`), the position of the input head in binary
 (`Turing.MultiTapeTM.encNat`), and a structure as the framed tuple of its fields.
 
-Reading, writing and moving on a zipper are tidily computable in linear time and space. A step of
+Reading, writing and moving on a zipper are computable in linear time and space
+(`Turing.MultiTapeTM.ComputableInDegree` with degrees one). A step of
 the simulation (`Turing.MultiTapeTM.Universal.step_inO`) takes space linear in the length `L` of
 the encoded context (the description, the input and the configuration). Its time bound separates
 the configuration length from description lookup and input scanning: for `K` work tapes, `E`
@@ -38,15 +40,23 @@ by `D`, even when the simulated configuration is large. The input scanner stream
 list with a binary countdown, whose arithmetic is charged to `P`. The configuration is still
 copied each round; this bound does not implement the buffered Hennie–Stearns simulation.
 
+`fun_prop` assembles a step from local rules that add up the bounds of the parts; only the
+transition lookup, `reads_inO`, `applyTapes_inO` and `moveInput_inO` carry hand-written bounds, and
+one comparison with `wTime` closes the step.
+
 ## Main definitions
 
 * `Turing.MultiTapeTM.Universal.eDesc`, `.eCfg`: the encodings of descriptions and configurations.
+* `Turing.MultiTapeTM.Universal.Ctx`, `.WCtx`: the contexts of a step, with and without the input,
+  and their named parts (`Ctx.desc`, `Ctx.input`, `Ctx.cfg`, `WCtx.desc`, `WCtx.cfg`, `WCtx.sym`).
 * `Turing.MultiTapeTM.Universal.stepTime`: the time bound of a step.
 
 ## Main results
 
-* `Turing.MultiTapeTM.Universal.step_inO`: a step is tidily computable within the time `stepTime`
-  and linear space.
+* `Turing.MultiTapeTM.Universal.step_inO`: a step is computable (`Turing.MultiTapeTM.ComputableInO`)
+  within the time `stepTime` and linear space.
+* `Turing.MultiTapeTM.Universal.stepWith_inO`, `.applyTapes_inO`, `.reads_inO`, `.moveInput_inO`:
+  its parts.
 -/
 
 namespace Turing.MultiTapeTM.Universal
@@ -110,7 +120,7 @@ public abbrev eCfgFields : Option ℕ × ℕ × List Tape ↪ List Bool :=
     eCfg c = eCfgFields (c.state, c.inputPos, c.workTapes) := rfl
 
 /-- The state of a configuration, in linear time. -/
-public lemma state_inO : ComputableTidilyInO SCfg.state eCfg eSym (fun c => (eCfg c).length)
+public lemma state_inO : ComputableInO SCfg.state eCfg eSym (fun c => (eCfg c).length)
     fun c => (eCfg c).length :=
   .of_linear (.of_unframe fun c => by simp [eCfg_apply])
 
@@ -118,60 +128,51 @@ public lemma state_inO : ComputableTidilyInO SCfg.state eCfg eSym (fun c => (eCf
 
 section Tape
 
-open ComputableTidilyInDegree
+open ComputableInDegree
 
-lemma tapeFields_deg : ComputableTidilyInDegree (fun t : Tape => (t.head, t.left, t.right)) eTape
+lemma tapeFields_deg : ComputableInDegree (fun t : Tape => (t.head, t.left, t.right)) eTape
     eTapeFields 1 1 :=
   of_eq fun _ => rfl
 
-@[local fun_prop]
-lemma tapeMk_deg : ComputableTidilyInDegree
+@[local fun_prop] lemma tapeMk_deg : ComputableInDegree
     (fun p : ℤ × List (Option ℕ) × List (Option ℕ) => Tape.mk p.1 p.2.1 p.2.2) eTapeFields eTape
     1 1 :=
   of_eq fun _ => rfl
 
-@[local fun_prop]
-lemma tapeHead_deg : ComputableTidilyInDegree Tape.head eTape encInt 1 1 :=
+@[local fun_prop] lemma tapeHead_deg : ComputableInDegree Tape.head eTape encInt 1 1 :=
   tapeFields_deg.fst'
 
-@[local fun_prop]
-lemma tapeLeft_deg : ComputableTidilyInDegree Tape.left eTape (encList eSym) 1 1 :=
+@[local fun_prop] lemma tapeLeft_deg : ComputableInDegree Tape.left eTape (encList eSym) 1 1 :=
   tapeFields_deg.snd'.fst'
 
-@[local fun_prop]
-lemma tapeRight_deg : ComputableTidilyInDegree Tape.right eTape (encList eSym) 1 1 :=
+@[local fun_prop] lemma tapeRight_deg : ComputableInDegree Tape.right eTape (encList eSym) 1 1 :=
   tapeFields_deg.snd'.snd'
 
 /-- The symbol under the head. -/
-@[local fun_prop]
-lemma read_deg : ComputableTidilyInDegree Tape.read eTape eSym 1 1 := by
+@[local fun_prop] lemma read_deg : ComputableInDegree Tape.read eTape eSym 1 1 := by
   unfold Tape.read
   fun_prop (disch := lia)
 
 /-- Writing under the head. -/
-@[local fun_prop]
-lemma write_deg : ComputableTidilyInDegree (fun p : Tape × Option ℕ => p.1.write p.2)
+@[local fun_prop] lemma write_deg : ComputableInDegree (fun p : Tape × Option ℕ => p.1.write p.2)
     (encPair eTape eSym) eTape 1 1 := by
   unfold Tape.write
   fun_prop (disch := lia)
 
 /-- A right move. -/
-@[local fun_prop]
-lemma movePos_deg :
-    ComputableTidilyInDegree (fun t : Tape => t.move .pos) eTape eTape 1 1 := by
+@[local fun_prop] lemma movePos_deg :
+    ComputableInDegree (fun t : Tape => t.move .pos) eTape eTape 1 1 := by
   simp only [Tape.move]
   fun_prop (disch := lia)
 
 /-- A left move. -/
-@[local fun_prop]
-lemma moveNeg_deg :
-    ComputableTidilyInDegree (fun t : Tape => t.move .neg) eTape eTape 1 1 := by
+@[local fun_prop] lemma moveNeg_deg :
+    ComputableInDegree (fun t : Tape => t.move .neg) eTape eTape 1 1 := by
   simp only [Tape.move]
   fun_prop (disch := lia)
 
 /-- Moving the head. -/
-@[local fun_prop]
-lemma move_deg : ComputableTidilyInDegree (fun p : Tape × SignType => p.1.move p.2)
+@[local fun_prop] lemma move_deg : ComputableInDegree (fun p : Tape × SignType => p.1.move p.2)
     (encPair eTape encSign) eTape 1 1 := by
   have ht := fst eTape encSign
   have hm := snd eTape encSign
@@ -184,10 +185,9 @@ lemma move_deg : ComputableTidilyInDegree (fun p : Tape × SignType => p.1.move
   rcases m with _ | _ | _ <;> rfl
 
 /-- Applying an action to a work tape: write, then move. -/
-@[local fun_prop]
-lemma apply_deg : ComputableTidilyInDegree (fun p : Tape × TapeAct =>
+@[local fun_prop] lemma apply_deg : ComputableInDegree (fun p : Tape × TapeAct =>
     p.1.apply p.2) (encPair eTape eTA) eTape 1 1 := by
-  convert (show ComputableTidilyInDegree (fun p : Tape × TapeAct =>
+  convert (show ComputableInDegree (fun p : Tape × TapeAct =>
     (if p.2.1.isSome then p.1.write (p.2.1.getD none) else p.1).move p.2.2)
     (encPair eTape eTA) eTape 1 1 by fun_prop (disch := first | apply le_refl | lia)) using 1
   funext ⟨t, w, m⟩
@@ -214,11 +214,11 @@ lemma foldl_applyStep (ts : List Tape) (as : List TapeAct) (acc : List Tape) :
     | nil => simp [applyStep, ih, applyTapes, applyTapes_nil_right]
     | cons a as => simp [applyStep, ih, applyTapes]
 
-lemma applyStep_deg : ComputableTidilyInDegree
+lemma applyStep_deg : ComputableInDegree
     (fun q : (List TapeAct × List Tape) × Tape => applyStep q.1 q.2)
     (encPair (encPair (encList eTA) (encList eTape)) eTape)
     (encPair (encList eTA) (encList eTape)) 1 1 := by
-  convert (show ComputableTidilyInDegree (fun q : (List TapeAct × List Tape) × Tape =>
+  convert (show ComputableInDegree (fun q : (List TapeAct × List Tape) × Tape =>
     (q.1.1.tail, q.1.2 ++ [if q.1.1.isEmpty then q.2 else q.2.apply (q.1.1.headD (none, 0))]))
     (encPair (encPair (encList eTA) (encList eTape)) eTape)
     (encPair (encList eTA) (encList eTape)) 1 1 by
@@ -291,12 +291,12 @@ lemma length_encList_map_read_le (ts : List Tape) :
 
 /-! ### All work tapes -/
 
-open ComputableTidilyInO
+open ComputableInO
 
 /-- Applying actions to the work tapes, within time the number of work tapes times the length of
 the arguments, and linear space. -/
 public theorem applyTapes_inO :
-    ComputableTidilyInO (fun p : List Tape × List TapeAct => applyTapes p.1 p.2)
+    ComputableInO (Function.uncurry applyTapes)
       (encPair (encList eTape) (encList eTA)) (encList eTape)
       (fun p => (p.1.length + 1) * ((encPair (encList eTape) (encList eTA) p).length + 1))
       fun p => (encPair (encList eTape) (encList eTA) p).length := by
@@ -312,9 +312,9 @@ public theorem applyTapes_inO :
     omega
   have hfold := (ComputableInO.foldl (encL := encList eTape)
     (encB := encPair (encList eTA) (encList eTape))
-    (fst (encList eTape) (encList eTA)).computableInO
-    ((snd (encList eTape) (encList eTA)).prod (const [])).computableInO
-    applyStep_deg.inO_one.computableInO
+    (fst (encList eTape) (encList eTA))
+    ((snd (encList eTape) (encList eTA)).prod (const []))
+    applyStep_deg.inO_one
     (R := fun p => 14 * (encPair (encList eTape) (encList eTA) p).length + 1)
     (Q := fun p => 14 * (encPair (encList eTape) (encList eTA) p).length + 1)
     (B := fun p => 6 * (encPair (encList eTape) (encList eTA) p).length)
@@ -328,19 +328,19 @@ public theorem applyTapes_inO :
       have h₂ := length_le_encList_of_mem eTape (List.getElem_mem hi)
       simp only [length_encPair] at h₁ h₂ ⊢
       omega)
-    (fun p i hi => hlen p i)).tidy
+    (fun p i hi => hlen p i))
   refine (((snd (encList eTA) (encList eTape)).comp_linear hfold).mono 32 (fun p => ?_)
     fun p => ?_).of_enc_eq fun p => ?_
   · simp only [length_encPair]
     nlinarith
   · simp only [length_encPair]
     omega
-  · simp [foldl_applyStep]
+  · simp [foldl_applyStep, Function.uncurry]
 
 /-- The symbols under the heads of the work tapes, within time the number of work tapes times
 their length, and linear space. -/
 public theorem reads_inO :
-    ComputableTidilyInO (fun ts : List Tape => ts.map Tape.read) (encList eTape) (encList eSym)
+    ComputableInO (fun ts : List Tape => ts.map Tape.read) (encList eTape) (encList eSym)
       (fun ts => (ts.length + 1) * ((encList eTape ts).length + 1))
       fun ts => (encList eTape ts).length := by
   refine ((mapWith (encP := encUnit) (f := fun p : Unit × Tape => p.2.read)
@@ -362,7 +362,7 @@ public theorem reads_inO :
 
 /-- Moving the input head, charging binary arithmetic only to the encoded position length. -/
 public theorem moveInput_inO :
-    ComputableTidilyInO (fun q : ℕ × Option ℕ × SignType => moveInput q.1 q.2.1 q.2.2)
+    ComputableInO (fun (p, a, m) => moveInput p a m)
       (encPair encNat (encPair eSym encSign)) encNat
       (fun q => (encPair encNat (encPair eSym encSign) q).length +
         ((encNat q.1).length + 1) ^ 2)
@@ -370,14 +370,14 @@ public theorem moveInput_inO :
   have hp := fst encNat (encPair eSym encSign)
   have ha := (snd encNat (encPair eSym encSign)).fst'
   have hm := (snd encNat (encPair eSym encSign)).snd'
-  have hsign (s : SignType) := (ComputableTidilyInDegree.of_finite (encIn := encSign)
+  have hsign (s : SignType) := (ComputableInDegree.of_finite (encIn := encSign)
     (encMid := encBool) fun m : SignType => decide (m = s)).inO_one.comp_linear hm
-  have hright := (ComputableTidilyInDegree.of_finite (encIn := encPair encBool encBool)
+  have hright := (ComputableInDegree.of_finite (encIn := encPair encBool encBool)
     (encMid := encBool) fun b : Bool × Bool => b.1 || b.2).inO_one.comp_linear
-      ((ComputableInO.natIsZero.tidy.comp_linear hp).prod
-        ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear ha))
-  refine (((hsign .zero).ite hp ((hsign .neg).ite (ComputableInO.natPred.tidy.comp hp)
-    (hright.ite (ComputableInO.natSucc.tidy.comp hp) hp))).mono 8 (fun q => ?_)
+      ((ComputableInO.natIsZero.comp_linear hp).prod
+        ((ComputableInDegree.isSome encUnary).inO_one.comp_linear ha))
+  refine (((hsign .zero).ite hp ((hsign .neg).ite (ComputableInO.natPred.comp hp)
+    (hright.ite (ComputableInO.natSucc.comp hp) hp))).mono 8 (fun q => ?_)
     fun q => ?_).of_enc_eq fun ⟨p, a, m⟩ => ?_
   · have h₁ : (encNat q.1).length ≤ (encPair encNat (encPair eSym encSign) q).length := by
       rw [length_encPair]; omega
@@ -400,13 +400,22 @@ public abbrev WCtx := (Desc × SCfg) × Option ℕ
 /-- The encoding of contexts without the input. -/
 public abbrev eWCtx : WCtx ↪ List Bool := encPair (encPair eDesc eCfg) eSym
 
+/-- The description of a context without the input. -/
+public abbrev WCtx.desc (c : WCtx) : Desc := c.1.1
+
+/-- The configuration of a context without the input. -/
+public abbrev WCtx.cfg (c : WCtx) : SCfg := c.1.2
+
+/-- The symbol under the input head, in a context without the input. -/
+public abbrev WCtx.sym (c : WCtx) : Option ℕ := c.2
+
 /-- The key of the transition to take. -/
 @[expose] public def wKey (c : WCtx) : Key :=
-  ⟨c.1.2.state.getD 0, c.2, c.1.2.workTapes.map Tape.read⟩
+  ⟨c.cfg.state.getD 0, c.sym, c.cfg.workTapes.map Tape.read⟩
 
 /-- The transition to take, if any. -/
 @[expose] public def wFound (c : WCtx) : Option (Key × Act) :=
-  c.1.1.table.find? (·.1 = wKey c)
+  c.desc.table.find? (·.1 = wKey c)
 
 /-- The default transition, never taken. -/
 @[expose] public def defaultEntry : Key × Act := (⟨0, none, []⟩, ⟨0, [], none, none⟩)
@@ -414,13 +423,13 @@ public abbrev eWCtx : WCtx ↪ List Bool := encPair (encPair eDesc eCfg) eSym
 /-- The action of the transition to take. -/
 @[expose] public def wAct (c : WCtx) : Act := ((wFound c).getD defaultEntry).2
 
-public lemma stepWith_eq (c : WCtx) : stepWith c.1.1 c.1.2 c.2 =
-    if c.1.2.state.isSome then
+public lemma stepWith_eq (c : WCtx) : stepWith c.desc c.cfg c.sym =
+    if c.cfg.state.isSome then
       (if (wFound c).isSome then
-        (⟨(wAct c).state, moveInput c.1.2.inputPos c.2 (wAct c).inputTape,
-          applyTapes c.1.2.workTapes (wAct c).workTapes⟩, (wAct c).output)
-        else (⟨none, c.1.2.inputPos, c.1.2.workTapes⟩, none))
-    else (c.1.2, none) := by
+        (⟨(wAct c).state, moveInput c.cfg.inputPos c.sym (wAct c).inputTape,
+          applyTapes c.cfg.workTapes (wAct c).workTapes⟩, (wAct c).output)
+        else (⟨none, c.cfg.inputPos, c.cfg.workTapes⟩, none))
+    else (c.cfg, none) := by
   obtain ⟨⟨d, ⟨_ | q, ip, ts⟩⟩, a⟩ := c
   · rfl
   · simp only [stepWith, Option.isSome_some, ↓reduceIte]
@@ -433,43 +442,43 @@ public lemma stepWith_eq (c : WCtx) : stepWith c.1.1 c.1.2 c.2 =
 /-- A step without input lookup: tape passes and description comparisons are linear in context
 length; only binary input-head arithmetic is quadratic in its own encoded length. -/
 @[expose] public def wTime (c : WCtx) : ℕ :=
-  (c.1.2.workTapes.length + c.1.1.table.length + 1) * ((eDesc c.1.1).length + 1) *
-    ((eWCtx c).length + 1) + ((encNat c.1.2.inputPos).length + 1) ^ 2
+  (c.cfg.workTapes.length + c.desc.table.length + 1) * ((eDesc c.desc).length + 1) *
+    ((eWCtx c).length + 1) + ((encNat c.cfg.inputPos).length + 1) ^ 2
 
 section Lengths
 
 variable (c : WCtx)
 
-lemma length_eWCtx : (eWCtx c).length = 2 * (2 * (eDesc c.1.1).length + 1 +
-    (2 * (eSym c.1.2.state).length + 1 + (2 * (encNat c.1.2.inputPos).length + 1 +
-      (encList eTape c.1.2.workTapes).length))) + 1 + (eSym c.2).length := by
+lemma length_eWCtx : (eWCtx c).length = 2 * (2 * (eDesc c.desc).length + 1 +
+    (2 * (eSym c.cfg.state).length + 1 + (2 * (encNat c.cfg.inputPos).length + 1 +
+      (encList eTape c.cfg.workTapes).length))) + 1 + (eSym c.sym).length := by
   simp only [eWCtx, eCfg_apply, length_encPair]
 
 lemma length_wTable_le :
-    (encList (encPair eKey eAct) c.1.1.table).length ≤ (eWCtx c).length := by
+    (encList (encPair eKey eAct) c.desc.table).length ≤ (eWCtx c).length := by
   rw [length_eWCtx]; simp only [eDesc_apply, length_encPair]; omega
 
 lemma length_le_wTime {A B k : ℕ}
-    (hA : A ≤ c.1.2.workTapes.length + c.1.1.table.length)
-    (hB : B ≤ (eWCtx c).length) (hk : k ≤ (eDesc c.1.1).length + 1) :
+    (hA : A ≤ c.cfg.workTapes.length + c.desc.table.length)
+    (hB : B ≤ (eWCtx c).length) (hk : k ≤ (eDesc c.desc).length + 1) :
     (A + 1) * k * (B + 1) ≤ wTime c :=
   (Nat.mul_le_mul (Nat.mul_le_mul (by omega) hk) (by omega)).trans (Nat.le_add_right _ _)
 
 /-- An entry of the table is no longer than the context. -/
-lemma length_le_of_mem_table {e : Key × Act} (he : e ∈ c.1.1.table) :
+lemma length_le_of_mem_table {e : Key × Act} (he : e ∈ c.desc.table) :
     (encPair eKey eAct e).length ≤ (eWCtx c).length :=
   (length_le_encList_of_mem (encPair eKey eAct) he).trans (length_wTable_le c)
 
 /-- An entry of the table is no longer than the description. -/
-lemma length_le_eDesc_of_mem_table {e : Key × Act} (he : e ∈ c.1.1.table) :
-    (encPair eKey eAct e).length ≤ (eDesc c.1.1).length := by
+lemma length_le_eDesc_of_mem_table {e : Key × Act} (he : e ∈ c.desc.table) :
+    (encPair eKey eAct e).length ≤ (eDesc c.desc).length := by
   have := length_le_encList_of_mem (encPair eKey eAct) he
   simp only [eDesc_apply, length_encPair] at *
   omega
 
 lemma length_wKey_le : (eKey (wKey c)).length ≤ 4 * (eWCtx c).length + 4 := by
-  have h₂ := length_encList_map_read_le c.1.2.workTapes
-  have h₃ : (c.1.2.state.getD 0) ≤ (eSym c.1.2.state).length := by cases c.1.2.state <;> simp
+  have h₂ := length_encList_map_read_le c.cfg.workTapes
+  have h₃ : (c.cfg.state.getD 0) ≤ (eSym c.cfg.state).length := by cases c.cfg.state <;> simp
   rw [length_eWCtx]
   simp only [wKey, eKey_apply, length_encPair, encUnary_apply, List.length_replicate]
   omega
@@ -490,160 +499,207 @@ lemma length_wAct_le : (eAct (wAct c)).length ≤ (eWCtx c).length + 6 := by
 
 end Lengths
 
-/-- A part of a step within the time `wTime` and linear space. -/
-abbrev WPart {β : Type} (f : WCtx → β) (enc : β ↪ List Bool) : Prop :=
-  ComputableTidilyInO f eWCtx enc wTime fun c => (eWCtx c).length
+/-! ### Rules for `fun_prop`
+
+Each rule adds up the time and space bounds of its arguments. -/
+
+section Rules
+
+variable {γ α : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool}
+  {T S T₁ S₁ T₂ S₂ T₃ S₃ : γ → ℕ}
+
+attribute [local fun_prop] ComputableInO ComputableInO.const ComputableInO.prod ComputableInO.fst'
+  ComputableInO.snd' ComputableInO.ite
+
+@[local fun_prop] lemma id_inO : ComputableInO (fun a : α => a) enc enc (fun a => (enc a).length)
+    fun a => (enc a).length :=
+  of_eq fun _ => rfl
+
+@[local fun_prop]
+lemma isSome_inO {o : γ → Option α} (h : ComputableInO o encIn (encOption enc) T S) :
+    ComputableInO (fun x => (o x).isSome) encIn encBool T S :=
+  (ComputableInDegree.isSome enc).inO_one.comp_linear h
+
+@[local fun_prop]
+lemma getD_inO {o : γ → Option α} (d : α) (h : ComputableInO o encIn (encOption enc) T S) :
+    ComputableInO (fun x => (o x).getD d) encIn enc T S :=
+  (ComputableInDegree.getD (enc₁ := enc) (enc := encOption enc) d).inO_one.comp_linear h
+
+variable {c : γ → SCfg} {a : γ → Act}
+
+@[local fun_prop] lemma cfgState_inO (h : ComputableInO c encIn eCfg T S) :
+    ComputableInO (fun x => (c x).state) encIn eSym T S :=
+  (h.of_enc_eq (encOut := eCfgFields) fun _ => rfl).fst'
+
+@[local fun_prop] lemma cfgInputPos_inO (h : ComputableInO c encIn eCfg T S) :
+    ComputableInO (fun x => (c x).inputPos) encIn encNat T S :=
+  (h.of_enc_eq (encOut := eCfgFields) fun _ => rfl).snd'.fst'
+
+@[local fun_prop] lemma cfgWorkTapes_inO (h : ComputableInO c encIn eCfg T S) :
+    ComputableInO (fun x => (c x).workTapes) encIn (encList eTape) T S :=
+  (h.of_enc_eq (encOut := eCfgFields) fun _ => rfl).snd'.snd'
+
+@[local fun_prop] lemma mkCfg_inO {s : γ → Option ℕ} {p : γ → ℕ} {ts : γ → List Tape}
+    (hs : ComputableInO s encIn eSym T₁ S₁) (hp : ComputableInO p encIn encNat T₂ S₂)
+    (ht : ComputableInO ts encIn (encList eTape) T₃ S₃) :
+    ComputableInO (fun x => (⟨s x, p x, ts x⟩ : SCfg)) encIn eCfg
+      (fun x => T₁ x + (T₂ x + T₃ x)) fun x => S₁ x + (S₂ x + S₃ x) :=
+  (hs.prod (hp.prod ht)).of_enc_eq fun _ => rfl
+
+/-- The fields of an action. -/
+abbrev eActFields := encPair encSign (encPair (encList eTA) (encPair eSym eSym))
+
+@[local fun_prop] lemma actInput_inO (h : ComputableInO a encIn eAct T S) :
+    ComputableInO (fun x => (a x).inputTape) encIn encSign T S :=
+  (h.of_enc_eq (encOut := eActFields) fun _ => rfl).fst'
+
+@[local fun_prop] lemma actWork_inO (h : ComputableInO a encIn eAct T S) :
+    ComputableInO (fun x => (a x).workTapes) encIn (encList eTA) T S :=
+  (h.of_enc_eq (encOut := eActFields) fun _ => rfl).snd'.fst'
+
+@[local fun_prop] lemma actOutput_inO (h : ComputableInO a encIn eAct T S) :
+    ComputableInO (fun x => (a x).output) encIn eSym T S :=
+  (h.of_enc_eq (encOut := eActFields) fun _ => rfl).snd'.snd'.fst'
+
+@[local fun_prop] lemma actState_inO (h : ComputableInO a encIn eAct T S) :
+    ComputableInO (fun x => (a x).state) encIn eSym T S :=
+  (h.of_enc_eq (encOut := eActFields) fun _ => rfl).snd'.snd'.snd'
+
+@[local fun_prop] lemma mkKey_inO {q : γ → ℕ} {i : γ → Option ℕ} {w : γ → List (Option ℕ)}
+    (hq : ComputableInO q encIn encUnary T₁ S₁) (hi : ComputableInO i encIn eSym T₂ S₂)
+    (hw : ComputableInO w encIn (encList eSym) T₃ S₃) :
+    ComputableInO (fun x => (⟨q x, i x, w x⟩ : Key)) encIn eKey
+      (fun x => T₁ x + (T₂ x + T₃ x)) fun x => S₁ x + (S₂ x + S₃ x) :=
+  (hq.prod (hi.prod hw)).of_enc_eq fun _ => rfl
+
+@[local fun_prop]
+lemma reads_inO' {ts : γ → List Tape} (h : ComputableInO ts encIn (encList eTape) T S) :
+    ComputableInO (fun x => (ts x).map Tape.read) encIn (encList eSym)
+      (fun x => T x + ((ts x).length + 1) * ((encList eTape (ts x)).length + 1))
+      fun x => S x + (encList eTape (ts x)).length :=
+  reads_inO.comp h
+
+@[local fun_prop] lemma moveInput_inO' {p : γ → ℕ} {i : γ → Option ℕ} {m : γ → SignType}
+    (hp : ComputableInO p encIn encNat T₁ S₁) (hi : ComputableInO i encIn eSym T₂ S₂)
+    (hm : ComputableInO m encIn encSign T₃ S₃) :
+    ComputableInO (fun x => moveInput (p x) (i x) (m x)) encIn encNat
+      (fun x => T₁ x + (T₂ x + T₃ x) + ((encPair encNat (encPair eSym encSign)
+        (p x, i x, m x)).length + ((encNat (p x)).length + 1) ^ 2))
+      fun x => S₁ x + (S₂ x + S₃ x) +
+        ((encPair encNat (encPair eSym encSign) (p x, i x, m x)).length + 1) :=
+  moveInput_inO.comp (hp.prod (hi.prod hm))
+
+@[local fun_prop] lemma applyTapes_inO' {ts : γ → List Tape} {as : γ → List TapeAct}
+    (ht : ComputableInO ts encIn (encList eTape) T₁ S₁)
+    (ha : ComputableInO as encIn (encList eTA) T₂ S₂) :
+    ComputableInO (fun x => applyTapes (ts x) (as x)) encIn (encList eTape)
+      (fun x => T₁ x + T₂ x + ((ts x).length + 1) *
+        ((encPair (encList eTape) (encList eTA) (ts x, as x)).length + 1))
+      fun x => S₁ x + S₂ x + (encPair (encList eTape) (encList eTA) (ts x, as x)).length :=
+  applyTapes_inO.comp (ht.prod ha)
+
+/-! ### A step without the input, assembled -/
 
 lemma le_wTime (c : WCtx) : (eWCtx c).length + 1 ≤ wTime c :=
   by simpa using length_le_wTime c (A := 0) (Nat.zero_le _) le_rfl (k := 1) (by omega)
 
-/-- One step of the simulation without the input, within the time `wTime` and linear space. -/
-public theorem stepWith_inO :
-    ComputableTidilyInO (fun c : WCtx => stepWith c.1.1 c.1.2 c.2) eWCtx (encPair eCfg eSym)
-      wTime fun c => (eWCtx c).length := by
-  -- the parts of the context
-  have hd := (fst (encPair eDesc eCfg) eSym).fst'
-  have hc := (fst (encPair eDesc eCfg) eSym).snd'
-  have hf := hc.of_enc_eq (encOut := eCfgFields)
-    (g := fun c : WCtx => (c.1.2.state, c.1.2.inputPos, c.1.2.workTapes)) fun _ => rfl
-  have htable := (hd.of_enc_eq (encOut := encPair encUnary (encPair encUnary
-    (encList (encPair eKey eAct)))) (g := fun c : WCtx => (c.1.1.tapes, c.1.1.q₀, c.1.1.table))
-    fun _ => rfl).snd'.snd'
-  -- the key
-  have hreads : WPart (fun c => c.1.2.workTapes.map Tape.read) (encList eSym) := by
-    refine (reads_inO.comp hf.snd'.snd').mono 2 (fun c => ?_) fun c => ?_
-    all_goals
-      have h₁ := length_eWCtx c
-      have h₂ := le_wTime c
-      have h₃ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega)
-        (B := (encList eTape c.1.2.workTapes).length) (by omega) (k := 1) (by omega)
-      simp only [eWCtx, Nat.mul_one] at *
-      omega
-  have hsym : WPart (fun c => c.2) eSym :=
-    (snd (encPair eDesc eCfg) eSym).mono 1 (fun c => by
-      have := le_wTime c; dsimp only [eWCtx] at *; omega) fun c => by dsimp only [eWCtx]; omega
-  have hkey : WPart wKey eKey := by
-    refine ((((ComputableTidilyInDegree.getD (enc₁ := encUnary) 0).inO_one.comp_linear
-      hf.fst').prod (hsym.prod hreads)).mono 4 (fun c => ?_) fun c => ?_).of_enc_eq
-      fun _ => rfl
-    all_goals
-      have := le_wTime c
-      dsimp only [eWCtx, Function.comp_apply] at *
-      omega
-  -- the transition
-  have htest := (ComputableInO.eq eKey).tidy.comp ((snd eKey (encPair eKey eAct)).fst'.prod
+/-- The key of the transition, within the time `wTime` and linear space. -/
+lemma wKey_inO : ComputableInO wKey eWCtx eKey wTime fun c => (eWCtx c).length := by
+  unfold wKey
+  refine .mono (by fun_prop) 8 (fun c => ?_) fun c => ?_
+  all_goals
+    have h₁ := length_eWCtx c
+    have h₂ := le_wTime c
+    have h₃ := length_le_wTime c (A := c.cfg.workTapes.length) (by omega)
+      (B := (encList eTape c.cfg.workTapes).length) (by omega) (k := 1) (by omega)
+    simp only [eWCtx, Nat.mul_one, length_encPair] at *
+    omega
+
+/-- The transition to take, within the time `wTime`: the key is compared with each entry of the
+table. A comparison costs the entry length times the key length, and the entry is bounded by the
+description. -/
+@[local fun_prop]
+lemma wFound_inO : ComputableInO wFound eWCtx (encOption (encPair eKey eAct)) wTime
+    fun c => (eWCtx c).length := by
+  have htable := ((fst (encPair eDesc eCfg) eSym).fst'.of_enc_eq
+    (encOut := encPair encUnary (encPair encUnary (encList (encPair eKey eAct))))
+    (g := fun c : WCtx => (c.desc.tapes, c.desc.q₀, c.desc.table)) fun _ => rfl).snd'.snd'
+  have htest := (ComputableInO.eq eKey).comp ((snd eKey (encPair eKey eAct)).fst'.prod
     (fst eKey (encPair eKey eAct)))
-  have hfound : WPart wFound (encOption (encPair eKey eAct)) := by
-    refine (findWith htest hkey htable).mono 64 (fun c => ?_) fun c => ?_
-    all_goals
-      have hk := length_wKey_le c
-      have ht := length_wTable_le c
-      have hst := le_wTime c
-      have hlinear : (eWCtx c).length + 1 ≤
-          ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) := by nlinarith
-      have hlen := length_le_length_encList (encPair eKey eAct) c.1.1.table
-    · have h₁ : listMax (fun e => (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
-          (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
-          ((eKey (e.1, wKey c).1).length + 1) *
-            ((eKey (e.1, wKey c).1).length + (eKey (e.1, wKey c).2).length + 1))
-          c.1.1.table ≤ 32 * ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) :=
-        listMax_le fun e he => by
-          have h₁ := length_le_of_mem_table c he
-          have h₂ := length_le_encPair_left eKey eAct e
-          have hD := length_le_eDesc_of_mem_table c he
-          have h₃ : ((eKey e.1).length + 1) * ((eKey e.1).length + (eKey (wKey c)).length + 1)
-              ≤ ((eDesc c.1.1).length + 1) * (5 * ((eWCtx c).length + 1)) :=
-            Nat.mul_le_mul (by omega) (by omega)
-          simp only [length_encPair] at *
-          nlinarith
-      have h₂ := length_le_wTime c (A := c.1.1.table.length) (by omega)
-        (B := (eWCtx c).length) le_rfl le_rfl
-      have h₃ := Nat.mul_le_mul_left (c.1.1.table.length + 1) (Nat.add_le_add
-        (Nat.add_le_add (hk.trans (show 4 * (eWCtx c).length + 4 ≤
-          4 * ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) by nlinarith))
-          (ht.trans (show (eWCtx c).length ≤
-            ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) by omega)))
-          h₁)
-      dsimp only [eWCtx, Function.comp_apply] at *
-      nlinarith
-    · have h₁ : listMax (fun e => (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
-          (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
-          (encPair eKey eKey (e.1, wKey c)).length) c.1.1.table ≤
-          32 * ((eWCtx c).length + 1) :=
-        listMax_le fun e he => by
-          have h₁ := length_le_of_mem_table c he
-          have h₂ := length_le_encPair_left eKey eAct e
-          simp only [length_encPair] at *
-          omega
-      dsimp only [eWCtx, Function.comp_apply] at *
-      omega
-  -- the action and the new configuration
-  have hact := (((ComputableTidilyInDegree.getD (enc₁ := encPair eKey eAct)
-    (enc := encOption (encPair eKey eAct)) defaultEntry).inO_one.comp_linear hfound).snd').of_enc_eq
-    (encOut := encPair encSign (encPair (encList eTA) (encPair eSym eSym)))
-    (g := fun c => ((wAct c).inputTape, (wAct c).workTapes, (wAct c).output,
-      (wAct c).state)) fun _ => rfl
-  have hmove : WPart (fun c => moveInput c.1.2.inputPos (wKey c).input (wAct c).inputTape)
-      encNat := by
-    have hinput := (hkey.of_enc_eq (encOut := encPair encUnary (encPair eSym (encList eSym)))
-      (g := fun c => ((wKey c).state, (wKey c).input, (wKey c).work)) fun _ => rfl)
-      |>.snd'.fst'
-    refine (moveInput_inO.comp (hf.snd'.fst'.prod (hinput.prod hact.fst'))).mono 256
-      (fun c => ?_) fun c => ?_
-    all_goals
-      have hk := length_wKey_le c
-      have ha := length_wAct_le c
-      have hst := le_wTime c
-      have hp : (encPair encNat (encPair eSym encSign) (c.1.2.inputPos, (wKey c).input,
-          (wAct c).inputTape)).length ≤ 8 * ((eWCtx c).length + 1) := by
-        have := length_eWCtx c
-        simp only [eKey_apply, eAct_apply, length_encPair] at *
-        omega
-      have h₂ : ((encNat c.1.2.inputPos).length + 1) ^ 2 ≤ wTime c :=
-        Nat.le_add_left _ _
-    · dsimp only [eWCtx, Function.comp_apply] at *
-      omega
-    · dsimp only [eWCtx, Function.comp_apply] at *
-      omega
-  have happ : WPart (fun c => applyTapes c.1.2.workTapes (wAct c).workTapes)
-      (encList eTape) := by
-    refine (applyTapes_inO.comp (hf.snd'.snd'.prod hact.snd'.fst')).mono 16 (fun c => ?_)
-      fun c => ?_
-    all_goals
-      have ha := length_wAct_le c
-      have hst := le_wTime c
-      have hp : (encPair (encList eTape) (encList eTA) (c.1.2.workTapes,
-          (wAct c).workTapes)).length ≤ 4 * ((eWCtx c).length + 1) := by
-        have := length_eWCtx c
-        simp only [eAct_apply, length_encPair] at *
+  refine (findWith htest wKey_inO htable).mono 64 (fun c => ?_) fun c => ?_
+  all_goals
+    have hk := length_wKey_le c
+    have ht := length_wTable_le c
+    have hst := le_wTime c
+    have hlinear : (eWCtx c).length + 1 ≤
+        ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) := by nlinarith
+    have hlen := length_le_length_encList (encPair eKey eAct) c.desc.table
+  · have h₁ : listMax (fun e => (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
+        (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
+        ((eKey (e.1, wKey c).1).length + 1) *
+          ((eKey (e.1, wKey c).1).length + (eKey (e.1, wKey c).2).length + 1))
+        c.desc.table ≤ 32 * ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) :=
+      listMax_le fun e he => by
+        have h₁ := length_le_of_mem_table c he
+        have h₂ := length_le_encPair_left eKey eAct e
+        have hD := length_le_eDesc_of_mem_table c he
+        have h₃ : ((eKey e.1).length + 1) * ((eKey e.1).length + (eKey (wKey c)).length + 1)
+            ≤ ((eDesc c.desc).length + 1) * (5 * ((eWCtx c).length + 1)) :=
+          Nat.mul_le_mul (by omega) (by omega)
+        simp only [length_encPair] at *
+        nlinarith
+    have h₂ := length_le_wTime c (A := c.desc.table.length) (by omega)
+      (B := (eWCtx c).length) le_rfl le_rfl
+    have h₃ := Nat.mul_le_mul_left (c.desc.table.length + 1) (Nat.add_le_add
+      (Nat.add_le_add (hk.trans (show 4 * (eWCtx c).length + 4 ≤
+        4 * ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) by nlinarith))
+        (ht.trans (show (eWCtx c).length ≤
+          ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) by omega)))
+        h₁)
+    dsimp only [eWCtx, Function.comp_apply] at *
+    nlinarith
+  · have h₁ : listMax (fun e => (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
+        (encPair eKey (encPair eKey eAct) (wKey c, e)).length +
+        (encPair eKey eKey (e.1, wKey c)).length) c.desc.table ≤
+        32 * ((eWCtx c).length + 1) :=
+      listMax_le fun e he => by
+        have h₁ := length_le_of_mem_table c he
+        have h₂ := length_le_encPair_left eKey eAct e
+        simp only [length_encPair] at *
         omega
-      have h₂ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega)
-        (B := (eWCtx c).length) le_rfl (k := 1) (by omega)
-      rw [Nat.mul_one] at h₂
-    · have h₁ := Nat.mul_le_mul_left (c.1.2.workTapes.length + 1) (Nat.add_le_add_right hp 1)
-      dsimp only [eWCtx, Function.comp_apply] at *
-      nlinarith
-    · dsimp only [eWCtx, Function.comp_apply] at *
-      omega
-  -- the result
-  have hlive := (((hact.snd'.snd'.snd'.prod (hmove.prod happ)).of_enc_eq (encOut := eCfg)
-    (g := fun c => (⟨(wAct c).state, moveInput c.1.2.inputPos (wKey c).input
-      (wAct c).inputTape, applyTapes c.1.2.workTapes (wAct c).workTapes⟩ : SCfg))
-    fun _ => rfl).prod hact.snd'.snd'.fst')
-  have hhalt := ((((const (encMid := eSym) none).prod hf.snd').of_enc_eq (encOut := eCfg)
-    (g := fun c : WCtx => (⟨none, c.1.2.inputPos, c.1.2.workTapes⟩ : SCfg)) fun _ => rfl).prod
-      (const (encMid := eSym) none))
-  have hidle := hc.prod (const (encMid := eSym) none)
-  refine ((((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear hf.fst').ite
-    (((ComputableTidilyInDegree.isSome (encPair eKey eAct)).inO_one.comp_linear hfound).ite
-      hlive hhalt) hidle).mono 16 (fun c => ?_) fun c => ?_).of_enc_eq fun c => ?_
-  · have := le_wTime c
     dsimp only [eWCtx, Function.comp_apply] at *
-    split_ifs <;> omega
-  · dsimp only [eWCtx, Function.comp_apply] at *
-    split_ifs <;> omega
-  · rw [stepWith_eq]
-    simp only [Function.comp_apply, wKey]
+    omega
+
+/-- The action of the transition to take, within the time `wTime`. -/
+@[local fun_prop]
+lemma wAct_inO : ComputableInO wAct eWCtx eAct wTime fun c => (eWCtx c).length := by
+  unfold wAct
+  fun_prop
+
+/-- One step of the simulation without the input, within the time `wTime` and linear space. -/
+public theorem stepWith_inO :
+    ComputableInO (fun c : WCtx => stepWith c.desc c.cfg c.sym) eWCtx (encPair eCfg eSym)
+      wTime fun c => (eWCtx c).length := by
+  simp only [stepWith_eq]
+  refine .mono (by fun_prop) 64 (fun c => ?_) fun c => ?_
+  all_goals
+    have hst := le_wTime c
+    have hl := length_eWCtx c
+    have ha := length_wAct_le c
+    simp only [eAct_apply, length_encPair] at ha
+    have hp : (encPair encNat (encPair eSym encSign)
+        (c.cfg.inputPos, c.sym, (wAct c).inputTape)).length ≤ 8 * ((eWCtx c).length + 1) := by
+      simp only [length_encPair] at *; omega
+    have ht : (encPair (encList eTape) (encList eTA)
+        (c.cfg.workTapes, (wAct c).workTapes)).length ≤ 4 * ((eWCtx c).length + 1) := by
+      simp only [length_encPair] at *; omega
+  · have hq : ((encNat c.cfg.inputPos).length + 1) ^ 2 ≤ wTime c := Nat.le_add_left _ _
+    have happ := length_le_wTime c (A := c.cfg.workTapes.length) (by omega)
+      (B := (eWCtx c).length) le_rfl (k := 1) (by omega)
+    have := Nat.mul_le_mul_left (c.cfg.workTapes.length + 1) (Nat.add_le_add_right ht 1)
+    rw [Nat.mul_one] at happ
+    split_ifs <;> nlinarith
+  · split_ifs <;> omega
 
 /-! ### A step -/
 
@@ -653,12 +709,21 @@ public abbrev Ctx := (Desc × List ℕ) × SCfg
 /-- The encoding of contexts. -/
 public abbrev eCtx : Ctx ↪ List Bool := encPair (encPair eDesc (encList encUnary)) eCfg
 
+/-- The description of a context. -/
+public abbrev Ctx.desc (c : Ctx) : Desc := c.1.1
+
+/-- The input of a context. -/
+public abbrev Ctx.input (c : Ctx) : List ℕ := c.1.2
+
+/-- The configuration of a context. -/
+public abbrev Ctx.cfg (c : Ctx) : SCfg := c.2
+
 /-- The step bound separates linear configuration passes from a streaming input lookup with
 binary countdown arithmetic. In particular, the whole configuration length is never squared. -/
 @[expose] public def stepTime (c : Ctx) : ℕ :=
-  (c.2.workTapes.length + c.1.1.table.length + 1) * ((eDesc c.1.1).length + 1) *
+  (c.cfg.workTapes.length + c.desc.table.length + 1) * ((eDesc c.desc).length + 1) *
     ((eCtx c).length + 1) +
-    ((encList encUnary c.1.2).length + 1) * ((encNat c.2.inputPos).length + 1) ^ 2
+    ((encList encUnary c.input).length + 1) * ((encNat c.cfg.inputPos).length + 1) ^ 2
 
 lemma le_stepTime_ctx (c : Ctx) : (eCtx c).length + 1 ≤ stepTime c :=
   (Nat.le_mul_of_pos_left _ (Nat.mul_pos (Nat.succ_pos _) (Nat.succ_pos _))).trans
@@ -667,7 +732,7 @@ lemma le_stepTime_ctx (c : Ctx) : (eCtx c).length + 1 ≤ stepTime c :=
 /-- One step of the simulation, on contexts, within the time `stepTime` and linear space: the
 symbol under the input head, and the step without the input. -/
 public theorem step_inO :
-    ComputableTidilyInO (fun c : Ctx => step c.1.1 c.1.2 c.2) eCtx (encPair eCfg eSym)
+    ComputableInO (fun c : Ctx => step c.desc c.input c.cfg) eCtx (encPair eCfg eSym)
       stepTime fun c => (eCtx c).length := by
   have hd := (fst (encPair eDesc (encList encUnary)) eCfg).fst'
   have hx := (fst (encPair eDesc (encList encUnary)) eCfg).snd'
@@ -675,7 +740,7 @@ public theorem step_inO :
   have hip := (hc.of_enc_eq (encOut := eCfgFields)
     (g := fun c : Ctx => (c.2.state, c.2.inputPos, c.2.workTapes)) fun _ => rfl).snd'.fst'
   refine ((stepWith_inO.comp
-    ((hd.prod hc).prod (inputSymbol_stream_inO.tidy.comp (hx.prod hip)))).mono 32
+    ((hd.prod hc).prod (inputSymbol_stream_inO.comp (hx.prod hip)))).mono 32
     (fun c => ?_) fun c => ?_).of_enc_eq fun c => by rw [step_eq_stepWith]; rfl
   all_goals
     have h₁ : (eSym (inputSymbol c.1.2 c.2.inputPos)).length ≤
@@ -703,4 +768,6 @@ public theorem step_inO :
   · dsimp only [eCtx, eWCtx] at *
     omega
 
+end Rules
+
 end Turing.MultiTapeTM.Universal
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean
index e313f253c9..87086cd031 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean
@@ -382,7 +382,8 @@ lemma halted_inO {α : Type} {enc : α ↪ List Bool} {c : α → SCfg} {T S : 
   ((ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
     fun b : Bool => !b).inO_one.comp_linear
       ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
-        (state_inO.comp_linear h))).of_enc_eq fun a => by
+        -- bridge for #862: tidy client of the plain `state_inO`
+        (state_inO.tidy.comp_linear h))).of_enc_eq fun a => by
         simp only [Function.comp_apply]
         cases (c a).state <;> rfl
 
@@ -435,7 +436,8 @@ public lemma stepG_inO :
   have hc := fst eCtl (encPair encNat encUnary)
   have hg := hc.fst'.fst'
   have hsym := countSym_inO (inputPos_inO hg.snd') hc.snd'.fst' hc.snd'.snd'
-  refine (stepWith_inO.comp (hg.prod (hsym.of_enc_eq (g := fun s : CSt => gSym s.1)
+  -- bridge for #862: tidy client of the plain `stepWith_inO`
+  refine (stepWith_inO.tidy.comp (hg.prod (hsym.of_enc_eq (g := fun s : CSt => gSym s.1)
     fun _ => rfl))).mono 100 (fun s => ?_) fun s => ?_
   all_goals
     have hw := wTime_le' (s.1.1.1, gSym s.1)
@@ -464,7 +466,8 @@ public lemma stepF_inO : ComputableTidilyInO (fun s : CSt => stepWith s.1.1.2.1
   have hn := snd eCtl (encPair encNat encUnary)
   have hg := hc.fst'.snd'
   have hsym := countSym_inO (inputPos_inO hg.snd') hn.fst' hn.snd'
-  refine (stepWith_inO.comp (hg.prod (hsym.of_enc_eq (g := xSym)
+  -- bridge for #862: tidy client of the plain `stepWith_inO`
+  refine (stepWith_inO.tidy.comp (hg.prod (hsym.of_enc_eq (g := xSym)
     fun _ => rfl))).mono 100 (fun s => ?_) fun s => ?_
   all_goals
     have hw := wTime_le' (s.1.1.2, xSym s)
@@ -619,7 +622,8 @@ public lemma cEmit_inO : ComputableTidilyInO (fun s : CSt => gEmit s.1) eCSt enc
 public lemma cCont_inO : ComputableTidilyInO (fun s : CSt => s.1.1.1.2.state.isSome) eCSt encBool
     (fun s => ((eCSt s).length + 1) ^ 3) fun s => (eCSt s).length + 1 :=
   (((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
-    (state_inO.comp_linear (fst eCtl (encPair encNat encUnary)).fst'.fst'.snd'))).mono 1
+    -- bridge for #862: tidy client of the plain `state_inO`
+    (state_inO.tidy.comp_linear (fst eCtl (encPair encNat encUnary)).fst'.fst'.snd'))).mono 1
     (fun s => by
       have hL : (eCSt s).length + 1 ≤ ((eCSt s).length + 1) ^ 3 := Nat.le_self_pow (by norm_num) _
       dsimp only [eCSt] at *
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean
index 99dd2094b0..bd5ab2cc97 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean
@@ -423,7 +423,7 @@ lemma wTime_le (s : St) : wTime (s.1, symAt s) ≤ 9 * ((eSt s).length + 1) ^ 3
     Nat.mul_le_mul (Nat.mul_le_mul hl (by omega)) (by omega)
   have hdigits := Nat.pow_le_pow_left (Nat.succ_le_succ hpos) 2
   unfold wTime
-  dsimp only at hproduct hdigits ⊢
+  dsimp only [WCtx.desc, WCtx.cfg] at hproduct hdigits ⊢
   nlinarith [Nat.le_self_pow (show 2 ≠ 0 by decide) ((eSt s).length + 1)]
 
 /-- The step at the end of a pass. -/
@@ -446,7 +446,8 @@ public lemma stepAt_inO : ComputableTidilyInO stepAt eSt (encPair eCfg eSym)
       (enc := eSym)).inO_one.comp_linear hcur)).of_enc_eq fun s => by
         simp only [symAt, Function.comp_apply]
         split_ifs <;> simp_all
-  have hstep := stepWith_inO.comp (hdc.prod hsym)
+  -- bridge for #862: tidy client of the plain `stepWith_inO`
+  have hstep := stepWith_inO.tidy.comp (hdc.prod hsym)
   have hidle := hc.prod (const (encMid := eSym) none)
   refine (((ComputableInO.natIsZero.tidy.comp_linear hr).ite hidle hstep).of_enc_eq (g := stepAt)
     fun s => ?_).mono 100 (fun s => ?_) fun s => ?_
@@ -527,7 +528,8 @@ public lemma foldFinish_inO : ComputableTidilyInO foldFinish eSt eHalted
   refine (((ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := eHalted)
     fun b : Bool => !b).inO_one.comp_linear
       ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
-        (state_inO.comp_linear hc))).of_enc_eq (g := foldFinish) fun s => by
+        -- bridge for #862: tidy client of the plain `state_inO`
+        (state_inO.tidy.comp_linear hc))).of_enc_eq (g := foldFinish) fun s => by
         simp only [foldFinish, Function.comp_apply]
         cases s.1.2.state <;> rfl).mono 1 (fun s => ?_) fun s => ?_ <;>
   · have hL : (eSt s).length + 1 ≤ ((eSt s).length + 1) ^ 3 := Nat.le_self_pow (by norm_num) _
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean
index 0e31d1e176..d256c024b6 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean
@@ -75,7 +75,8 @@ lemma round_inO : ComputableTidilyInO round eRun eRun (fun s => stepTime s.1 + (
     fun s => (eRun s).length := by
   have hctx := fst eCtx (encList encUnary)
   have hout := snd eCtx (encList encUnary)
-  have hstep := step_inO.comp hctx
+  -- bridge for #862: tidy client of the plain `step_inO`
+  have hstep := step_inO.tidy.comp hctx
   have hnewout := ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
     hstep.snd').ite ((ComputableTidilyInDegree.snoc encUnary).inO_one.comp_linear
       (hout.prod ((ComputableTidilyInDegree.getD (enc₁ := encUnary) 0).inO_one.comp_linear
@@ -206,7 +207,8 @@ public theorem computableTidilyInO_universal :
       exact length_eRun_le i.1 i.2.1 hk)).tidy
   have hhalted := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
     (fun b : Bool => !b)).inO_one.comp_linear ((ComputableTidilyInDegree.isSome encUnary).inO_one
-      |>.comp_linear (state_inO.comp_linear hiter.fst'.snd'))
+      -- bridge for #862: tidy client of the plain `state_inO`
+      |>.comp_linear (state_inO.tidy.comp_linear hiter.fst'.snd'))
   refine ((hiter.snd'.prod hhalted).mono 16 (fun i => ?_) fun i => ?_).of_enc_eq fun i => ?_
   · have h₁ : (eDesc i.1).length ≤ (eIn i).length := length_le_encPair_left _ _ i
     have h₂ := Nat.pow_le_pow_left (Nat.add_le_add_right h₁ 1) 2
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean
index 0d137351e2..2f45c61746 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean
@@ -516,7 +516,8 @@ private lemma foldFinishS_inO : ComputableTidilyInO foldFinishS eSSt eOut
     (fun s => ((eSSt s).length + 1) ^ 3) fun s => (eSSt s).length + 1 := by
   have h₁ := fst eSt (encPair encUnary (encList encUnary))
   have h₂ := snd eSt (encPair encUnary (encList encUnary))
-  have hst := state_inO.comp_linear h₁.fst'.snd'
+  -- bridge for #862: tidy client of the plain `state_inO`
+  have hst := state_inO.tidy.comp_linear h₁.fst'.snd'
   have hnone := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
     fun b : Bool => !b).inO_one.comp_linear
       ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear hst)
diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json
index 0ccd7185cf..e20fbe018c 100644
--- a/scripts/tidy_surface_baseline.json
+++ b/scripts/tidy_surface_baseline.json
@@ -52,7 +52,6 @@
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5,
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2,
  "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2,
- "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 6,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9,