diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean
index 292d05d43..09e06559b 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 0d96f3221..f72978176 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`
@@ -41,12 +43,16 @@ copied each round; this bound does not implement the buffered Hennie–Stearns s
 ## 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 +116,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,39 +124,39 @@ 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
+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 :=
+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 :=
+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 :=
+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
+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)
+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)
@@ -158,20 +164,20 @@ lemma write_deg : ComputableTidilyInDegree (fun p : Tape × Option ℕ => p.1.wr
 /-- A right move. -/
 @[local fun_prop]
 lemma movePos_deg :
-    ComputableTidilyInDegree (fun t : Tape => t.move .pos) eTape eTape 1 1 := by
+    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
+    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)
+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
@@ -185,9 +191,9 @@ lemma move_deg : ComputableTidilyInDegree (fun p : Tape × SignType => p.1.move
 
 /-- Applying an action to a work tape: write, then move. -/
 @[local fun_prop]
-lemma apply_deg : ComputableTidilyInDegree (fun p : Tape × TapeAct =>
+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 +220,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 +297,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 +318,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 +334,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 +368,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 +376,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 +406,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 +429,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 +448,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
@@ -492,38 +507,38 @@ 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
+  ComputableInO f eWCtx enc wTime fun c => (eWCtx c).length
 
 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)
+    ComputableInO (fun c : WCtx => stepWith c.desc c.cfg c.sym) 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
+    (g := fun c : WCtx => (c.cfg.state, c.cfg.inputPos, c.cfg.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))
+    (encList (encPair eKey eAct)))) (g := fun c : WCtx => (c.desc.tapes, c.desc.q₀, c.desc.table))
     fun _ => rfl).snd'.snd'
   -- the key
-  have hreads : WPart (fun c => c.1.2.workTapes.map Tape.read) (encList eSym) := by
+  have hreads : WPart (fun c => c.cfg.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)
+      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] at *
       omega
-  have hsym : WPart (fun c => c.2) eSym :=
+  have hsym : WPart (fun c => c.sym) 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
+    refine ((((ComputableInDegree.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
@@ -531,7 +546,7 @@ public theorem stepWith_inO :
       dsimp only [eWCtx, Function.comp_apply] at *
       omega
   -- the transition
-  have htest := (ComputableInO.eq eKey).tidy.comp ((snd eKey (encPair eKey eAct)).fst'.prod
+  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 => ?_
@@ -540,35 +555,35 @@ public theorem stepWith_inO :
       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
+          ((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.1.1.table ≤ 32 * ((eDesc c.1.1).length + 1) * ((eWCtx c).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.1.1).length + 1) * (5 * ((eWCtx 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.1.1.table.length) (by omega)
+      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.1.1.table.length + 1) (Nat.add_le_add
+      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.1.1).length + 1) * ((eWCtx c).length + 1) by nlinarith))
+          4 * ((eDesc c.desc).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)))
+            ((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.1.1.table ≤
+          (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
@@ -578,12 +593,12 @@ public theorem stepWith_inO :
       dsimp only [eWCtx, Function.comp_apply] at *
       omega
   -- the action and the new configuration
-  have hact := (((ComputableTidilyInDegree.getD (enc₁ := encPair eKey eAct)
+  have hact := (((ComputableInDegree.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)
+  have hmove : WPart (fun c => moveInput c.cfg.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)
@@ -594,48 +609,48 @@ public theorem stepWith_inO :
       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,
+      have hp : (encPair encNat (encPair eSym encSign) (c.cfg.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 :=
+      have h₂ : ((encNat c.cfg.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)
+  have happ : WPart (fun c => applyTapes c.cfg.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,
+      have hp : (encPair (encList eTape) (encList eTA) (c.cfg.workTapes,
           (wAct c).workTapes)).length ≤ 4 * ((eWCtx c).length + 1) := by
         have := length_eWCtx c
         simp only [eAct_apply, length_encPair] at *
         omega
-      have h₂ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega)
+      have h₂ := length_le_wTime c (A := c.cfg.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)
+    · have h₁ := Nat.mul_le_mul_left (c.cfg.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))
+    (g := fun c => (⟨(wAct c).state, moveInput c.cfg.inputPos (wKey c).input
+      (wAct c).inputTape, applyTapes c.cfg.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
+    (g := fun c : WCtx => (⟨none, c.cfg.inputPos, c.cfg.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
+  refine ((((ComputableInDegree.isSome encUnary).inO_one.comp_linear hf.fst').ite
+    (((ComputableInDegree.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 *
@@ -653,12 +668,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 +691,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 +699,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 ≤
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean
index e313f253c..87086cd03 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 99dd2094b..bd5ab2cc9 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 0e31d1e17..d256c024b 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 0d137351e..2f45c6174 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 0ccd7185c..e20fbe018 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,