diff --git a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean
index a1cdd4e02a..d94ad11a16 100644
--- a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean
+++ b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean
@@ -12,7 +12,7 @@ import Complexity.Computability.Complexity.FineGrained.CountingSparsificationUni
 import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds
 import Complexity.Computability.PolyTime.FineGrained.ParameterCheck
 import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime
-import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
@@ -71,7 +71,6 @@ namespace Cslib.Complexity.CountingNativeEndpointPrep
 open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification
 open Cslib.Logic.PL.CNF (validDeclaredInput validDeclaredInput_eq_true_iff)
 open Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM
-open Turing.MultiTapeTM.Universal (encUnit encUnit_apply)
 open CountingSparsify SubexponentialSAT SubexponentialSAT.ReplacementParams
 open SubexponentialSAT.SparseCountingScale Filter
 
@@ -426,7 +425,6 @@ namespace Cslib.Complexity.CountingNativeEndpointPrep
 
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.CNF.Sparsification
 open Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM Cslib.GenericRAM
-open Turing.MultiTapeTM.Universal (encUnit encUnit_apply)
 open CountingSparsify SubexponentialSAT SubexponentialSAT.SparsePolyCounter
 open BranchedSparseCNFCounter
 
diff --git a/Complexity/Computability/Machines/ReadMachine/Tidy.lean b/Complexity/Computability/Machines/ReadMachine/Tidy.lean
index 60828dc5ce..f5aad45281 100644
--- a/Complexity/Computability/Machines/ReadMachine/Tidy.lean
+++ b/Complexity/Computability/Machines/ReadMachine/Tidy.lean
@@ -279,16 +279,16 @@ theorem toStepMachine_resourceCertificate (hhalt : ComputableInO m.halt encS enc
       (budget_prod hisN (budget_prod he (budget_prod hl (budget_prod ha hz)))) hst
     -- the three results
     have hres₁ := budget_prod (encB := encPair encS encNat) (budget_prod (fst' hr) hpos)
-      (budget_prod (encB := encMove) (budget_const (0 : SignType) hin hst) (snd' hr))
+      (budget_prod (encB := encSign) (budget_const (0 : SignType) hin hst) (snd' hr))
     have hres₂ := budget_prod (encB := encPair encS encNat) (budget_prod hq
       (budget_comp natSucc hpos (sq_bigOLe hpos.length_le)
         (.add hpos.length_le (.const 1 _))))
-      (budget_prod (encB := encMove) (budget_const (1 : SignType) hin hst)
+      (budget_prod (encB := encSign) (budget_const (1 : SignType) hin hst)
         (budget_const (encB := encBits) ([] : List Bool) hin hst))
     have hres₃ := budget_prod (encB := encPair encS encNat) (budget_prod hq
       (budget_comp natPred hpos (sq_bigOLe hpos.length_le)
         (.add hpos.length_le (.const 1 _))))
-      (budget_prod (encB := encMove) (budget_const (-1 : SignType) hin hst)
+      (budget_prod (encB := encSign) (budget_const (-1 : SignType) hin hst)
         (budget_const (encB := encBits) ([] : List Bool) hin hst))
     have hall := budget_ite hc hres₁ (budget_ite hl hres₂ hres₃)
     refine ((hall.of_enc_eq fun p => by rw [← stepBy_eq]; rfl).mono 4 (fun p => ?_)
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean
index 5a6a6d76ed..68c387f5fb 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean
@@ -82,6 +82,14 @@ public lemma length_encInt (z : ℤ) :
     (encInt z).length = if z < 0 then (-z).toNat else z.toNat + 1 := by
   rcases z with n | n <;> simp [Int.negSucc_lt_zero]
 
+public lemma length_encInt_add_one_le (z : ℤ) :
+    (encInt (z + 1)).length ≤ (encInt z).length + 1 := by
+  rw [length_encInt, length_encInt]; split_ifs <;> omega
+
+public lemma length_encInt_sub_one_le (z : ℤ) :
+    (encInt (z - 1)).length ≤ (encInt z).length + 1 := by
+  rw [length_encInt, length_encInt]; split_ifs <;> omega
+
 namespace EncInt
 
 /-- Adds one to an encoded integer. -/
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean
index e8a1cead52..30b0f7e6b5 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean
@@ -8,10 +8,17 @@ module
 -- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted)
 
 public import Complexity.Init
+public import Mathlib.Basic.Sign.Defs
 public import Mathlib.Data.List.Basic
 public import Mathlib.Logic.Embedding.Basic
 
-/-! # The single-symbol encoding of Booleans -/
+/-!
+# Encodings of Booleans, signs and the unit type
+
+`Turing.MultiTapeTM.encBool` encodes a Boolean by one symbol, `Turing.MultiTapeTM.encSign` a sign,
+such as a head move, by at most one symbol, and `Turing.MultiTapeTM.encUnit` the unit by the empty
+word.
+-/
 
 namespace Turing.MultiTapeTM
 
@@ -22,4 +29,16 @@ namespace Turing.MultiTapeTM
 @[simp]
 public lemma encBool_apply (b : Bool) : encBool b = [b] := rfl
 
+/-- Signs: `0 ↦ []`, `-1 ↦ [false]` and `1 ↦ [true]`. -/
+@[expose] public def encSign : SignType ↪ List Bool :=
+  ⟨fun m => match m with | .zero => [] | .neg => [false] | .pos => [true], by
+    intro a b h
+    cases a <;> cases b <;> simp_all⟩
+
+/-- The unit type, encoded by the empty word. -/
+@[expose] public def encUnit : Unit ↪ List Bool := ⟨fun _ => [], fun _ _ _ => rfl⟩
+
+@[simp]
+public lemma encUnit_apply (u : Unit) : encUnit u = [] := rfl
+
 end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean
index c6827e2bca..ed42a6105b 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean
@@ -213,23 +213,23 @@ lemma moveOn_eq (n p : ℕ) (d : SignType) :
 
 /-- **The head of `g` after a move**, in quadratic time and linear space. -/
 lemma moveOn_inO : ComputableInO (fun q : ℕ × ℕ × SignType => moveOn q.1 q.2.1 q.2.2)
-    (encPair encNat (encPair encNat encMove)) encNat
-    (fun q => ((encPair encNat (encPair encNat encMove) q).length + 1) ^ 2)
-    fun q => (encPair encNat (encPair encNat encMove) q).length + 1 := by
-  have hn := fst encNat (encPair encNat encMove)
-  have hp := (snd encNat (encPair encNat encMove)).fst'
-  have hd := (snd encNat (encPair encNat encMove)).snd'
-  have hdz := (ComputableInDegree.of_finite (encIn := encMove) (encMid := encBool)
+    (encPair encNat (encPair encNat encSign)) encNat
+    (fun q => ((encPair encNat (encPair encNat encSign) q).length + 1) ^ 2)
+    fun q => (encPair encNat (encPair encNat encSign) q).length + 1 := by
+  have hn := fst encNat (encPair encNat encSign)
+  have hp := (snd encNat (encPair encNat encSign)).fst'
+  have hd := (snd encNat (encPair encNat encSign)).snd'
+  have hdz := (ComputableInDegree.of_finite (encIn := encSign) (encMid := encBool)
     fun d : SignType => decide (d = 0)).inO_one.comp_linear hd
-  have hdn := (ComputableInDegree.of_finite (encIn := encMove) (encMid := encBool)
+  have hdn := (ComputableInDegree.of_finite (encIn := encSign) (encMid := encBool)
     fun d : SignType => decide (d = -1)).inO_one.comp_linear hd
   have heq := (eq encNat).comp (hp.prod (natSucc.comp hn))
   have h := hdz.ite hp (hdn.ite (natPred.comp hp) (heq.ite hp (natSucc.comp hp)))
   refine (h.of_enc_eq fun q => ?_).mono 16 (fun q => ?_) fun q => ?_
   · simp only [moveOn_eq, Function.comp_apply, decide_eq_true_eq]
   all_goals
-    have h₁ := length_encPair (enc₁ := encNat) (enc₂ := encPair encNat encMove) q
-    have h₂ := length_encPair (enc₁ := encNat) (enc₂ := encMove) q.2
+    have h₁ := length_encPair (enc₁ := encNat) (enc₂ := encPair encNat encSign) q
+    have h₂ := length_encPair (enc₁ := encNat) (enc₂ := encSign) q.2
     have h₃ := (show (encNat (q.2.1 - 1)).length ≤ (encNat q.2.1).length from by
       simpa [Nat.size_eq_bits_len] using Nat.size_le_size (Nat.sub_le q.2.1 1))
     have h₄ := ComputableTidilyInO.length_encNat_add_le q.1 1
@@ -324,7 +324,7 @@ variable {f : StepMachine σf Bool Bool} {g : StepMachine σg Bool Bool} {Tf Sf
 local notation "encArg" => encPair (encCompState encF encG) (encOption encBool)
 
 /-- The encoding of the results of a step. -/
-local notation "encRes" => encPair (encCompState encF encG) (encPair encMove encBits)
+local notation "encRes" => encPair (encCompState encF encG) (encPair encSign encBits)
 
 lemma length_encArg_le (p : CompState σf σg × Option Bool) :
     (encArg p).length ≤ 2 * (encCompState encF encG p.1).length + 3 := by
@@ -403,8 +403,8 @@ lemma stepF_inO (hf : f.ResourceCertificate encF Tf Sf) :
   have hn : (fun p : CompState σf σg × Option Bool => (f.step p.1.f p.2).2.2.length) ≼
       fun p => Sf p.1.f + (encCompState encF encG p.1).length := .of_le_linear cf cf fun p => by
     have := hcf (p.1.f, p.2)
-    have := length_le_encPair_right encF (encPair encMove encBits) (f.step p.1.f p.2)
-    have := length_le_encPair_right encMove encBits (f.step p.1.f p.2).2
+    have := length_le_encPair_right encF (encPair encSign encBits) (f.step p.1.f p.2)
+    have := length_le_encPair_right encSign encBits (f.step p.1.f p.2).2
     simp only [encBits_apply] at *
     nlinarith
   have hA := (encArg_bigO (encF := encF) (encG := encG)).trans
@@ -431,7 +431,7 @@ lemma stepF_inO (hf : f.ResourceCertificate encF Tf Sf) :
 lemma stepG_round_inO (hg : g.ResourceCertificate encG Tg Sg) :
     ComputableInO
       (fun p : CompState σf σg × Option Bool => g.step p.1.g.1 (p.1.cd.symbol p.1.g.2))
-      encArg (encPair encG (encPair encMove encBits))
+      encArg (encPair encG (encPair encSign encBits))
       (fun p => 4 * (encArg p).length + Tg p.1.g.1)
       (fun p => 4 * (encArg p).length + Sg p.1.g.1) := by
   have hs := fst (encCompState encF encG) (encOption encBool)
@@ -456,10 +456,10 @@ lemma stepG_head_inO (hg : g.ResourceCertificate encG Tg Sg) :
         moveOn p.1.cd.len p.1.g.2 (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)
       encArg encNat
       (fun p => 6 * (encArg p).length + Tg p.1.g.1 +
-        ((encPair encNat (encPair encNat encMove)
+        ((encPair encNat (encPair encNat encSign)
           (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length + 1) ^ 2)
       (fun p => 6 * (encArg p).length + Sg p.1.g.1 +
-        (encPair encNat (encPair encNat encMove)
+        (encPair encNat (encPair encNat encSign)
           (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length + 1) := by
   have hs := fst (encCompState encF encG) (encOption encBool)
   have hgp := CompState.g_inO.comp_linear hs
@@ -492,11 +492,11 @@ lemma stepG_inO (hg : g.ResourceCertificate encG Tg Sg) :
   obtain ⟨hgs, hpg, hlen, -⟩ := parts_bigO (encF := encF) (encG := encG)
   have hA := encArg_bigO (encF := encF) (encG := encG)
   have hmv : (fun p : CompState σf σg × Option Bool =>
-      (encMove (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1).length) ≼
+      (encSign (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1).length) ≼
         fun p => (encCompState encF encG p.1).length :=
     .of_le_linear 0 1 fun p => by
-      cases (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1 <;> simp [encMove]
-  have hsq : (fun p : CompState σf σg × Option Bool => ((encPair encNat (encPair encNat encMove)
+      cases (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1 <;> simp [encSign]
+  have hsq : (fun p : CompState σf σg × Option Bool => ((encPair encNat (encPair encNat encSign)
       (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length + 1) ^ 2) ≼
         fun p => ((encCompState encF encG p.1).length + 1) ^ 3 :=
     BigOLe.pow_le (by simp only [length_encPair]; bigO)
@@ -508,11 +508,11 @@ lemma stepG_inO (hg : g.ResourceCertificate encG Tg Sg) :
     (BigOLe.of_le fun p => Nat.pow_le_pow_left (by omega) 3).trans hT
   have hAt := hA.trans hL
   have hAs := hA.trans hLs
-  have hlin : (fun p : CompState σf σg × Option Bool => (encPair encNat (encPair encNat encMove)
+  have hlin : (fun p : CompState σf σg × Option Bool => (encPair encNat (encPair encNat encSign)
       (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length) ≼
         fun p => compSpace encF encG Sf Sg p.1 :=
     BigOLe.trans (by simp only [length_encPair]; bigO) hLs
-  refine (hst.prod ((const (0 : SignType) (encMid := encMove)).prod hr.snd'.snd')).weaken ?_ ?_ <;>
+  refine (hst.prod ((const (0 : SignType) (encMid := encSign)).prod hr.snd'.snd')).weaken ?_ ?_ <;>
   · bigO
 
 lemma le_compTime (s : CompState σf σg) :
@@ -557,7 +557,7 @@ lemma rewind_inO : ComputableInO (fun p : CompState σf σg × Option Bool =>
         (⟨p.1.g, p.1.phase, p.1.f, p.1.cd⟩ : CompState σf σg)) fun p => rfl
   have hres {st : CompState σf σg × Option Bool → CompState σf σg} {T S}
       (h : ComputableInO st encArg (encCompState encF encG) T S) (d : SignType) :=
-    h.prod ((const d (encMid := encMove)).prod (const ([] : List Bool) (encMid := encBits)))
+    h.prod ((const d (encMid := encSign)).prod (const ([] : List Bool) (encMid := encBits)))
   have hAt := (encArg_bigO (encF := encF) (encG := encG)).trans
     (time_bigO (Tf := Tf) (Sf := Sf) (Tg := Tg)).2.1
   have hAs := (encArg_bigO (encF := encF) (encG := encG)).trans (space_bigO (Sf := Sf) (Sg := Sg)).1
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean
index 9f01d6ad26..8a7fde3ac9 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean
@@ -15,6 +15,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Ste
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OnWords
 public import Complexity.Computability.Machines.Turing.MultiTape.StepMachine.Basic
 public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant
@@ -34,7 +35,7 @@ an unbounded output with constant workspace; no bound on the whole output is add
 
 ## Main definitions
 
-* `Turing.MultiTapeTM.encMove`, `.encPeek`: the unchanged encodings used by the compiler.
+* `Turing.MultiTapeTM.encPeek`: the unchanged encoding used by the compiler.
 * `Turing.StepMachine.ResourceCertificate`: charged plain certificates for halt and step.
 
 ## Main results
@@ -55,13 +56,7 @@ public lemma linear_stepFlagWord :
     ComputableInLinearTimeAndSpace stepFlagWord encBool encBits :=
   .of_finite stepFlagWord
 
-/-- Moves of the input head: none, to the left, to the right. -/
-@[expose] public def encMove : SignType ↪ List Bool :=
-  ⟨fun m => match m with | .zero => [] | .neg => [false] | .pos => [true], by
-    intro a b h
-    cases a <;> cases b <;> simp_all⟩
-
-@[simp] public lemma moveOfCell_encMove (m : SignType) : moveOfCell (encMove m).head? = m := by
+@[simp] public lemma moveOfCell_encSign (m : SignType) : moveOfCell (encSign m).head? = m := by
   cases m <;> rfl
 
 public lemma peekWord_injective : Function.Injective peekWord := by
@@ -164,14 +159,14 @@ variable {σ : Type} {encS : σ ↪ List Bool} {halt : σ → Bool}
   {TS SS : σ × Option Bool → ℕ}
 
 /-- The state and its pending move. -/
-public abbrev encAug (encS : σ ↪ List Bool) : σ × SignType ↪ List Bool := encPair encS encMove
+public abbrev encAug (encS : σ ↪ List Bool) : σ × SignType ↪ List Bool := encPair encS encSign
 
 /-- The step, read from the state behind the symbol under the input head. -/
 lemma step_peek_inO
     (hstep : ComputableInO (fun p : σ × Option Bool => step p.1 p.2)
-      (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits)) TS SS) :
+      (encPair encS (encOption encBool)) (encPair encS (encPair encSign encBits)) TS SS) :
     ComputableInO (fun p : Option Bool × (σ × SignType) => step p.2.1 p.1)
-      (encPeek (encAug encS)) (encPair encS (encPair encMove encBits))
+      (encPeek (encAug encS)) (encPair encS (encPair encSign encBits))
       (fun p => (encPeek (encAug encS) p).length + (encPeek (encAug encS) p).length +
         TS (p.2.1, p.1))
       fun p => (encPeek (encAug encS) p).length + (encPeek (encAug encS) p).length +
@@ -247,7 +242,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis
     (hinit : ComputableInO init encIn encS TI SI)
     (hhalt : ComputableInO halt encS encBool TH SH)
     (hstep : ComputableInO (fun p : σ × Option Bool => step p.1 p.2)
-      (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits)) TS SS)
+      (encPair encS (encOption encBool)) (encPair encS (encPair encSign encBits)) TS SS)
     (hrounds : ∀ x, (StepMachine.mk (init x) halt step).HaltsAt (encIn x) (rounds x))
     (hg : ∀ x, encOut (g x) =
       ((StepMachine.mk (init x) halt step).run (encIn x) (rounds x)).out)
@@ -337,16 +332,16 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis
   have hP (b : Option Bool) (n : ℕ) (hn : n ≤ R) (mm : SignType) :
       (encPeek (encAug encS) (b, (q n, mm))).length ≤ 2 * L + 4 := by
     have : (encS (q n)).length ≤ L := hlMax x n hn
-    cases b <;> cases mm <;> simp [peekWord, encMove] <;> omega
+    cases b <;> cases mm <;> simp [peekWord, encSign] <;> omega
   have hst (n : ℕ) (hn : n ≤ R) : TS (q n, a n) + TH (q n) ≤ Tm ∧ SS (q n, a n) + SH (q n) ≤ Sm :=
     ⟨htMax x n hn, hsMax x n hn⟩
   have hfl (n : ℕ) : (stepFlagWord (!halt (q n))).length ≤ 1 := by
     unfold stepFlagWord; split_ifs <;> simp
-  have hmv (mm : SignType) : (encMove mm).length ≤ 1 := by cases mm <;> simp [encMove]
+  have hmv (mm : SignType) : (encSign mm).length ≤ 1 := by cases mm <;> simp [encSign]
   have h := computesTidily_stepTM hVN hVF hNF hVC hVM w R (fun n => encAug encS (q n, mv n))
-    (fun n => (st n).2.2) (fun n => encMove (st n).2.1) (fun n => stepFlagWord (!halt (q n)))
+    (fun n => (st n).2.2) (fun n => encSign (st n).2.1) (fun n => stepFlagWord (!halt (q n)))
     (fun n => (m.run w n).pos) rfl
-    (fun n hn => by simp only [hrun n hn, moveOfCell_encMove])
+    (fun n hn => by simp only [hrun n hn, moveOfCell_encSign])
     (fun n hn => by simp [hnh n hn, stepFlagWord])
     (by simpa [stepFlagWord] using (hrounds x).1)
     ((hI x).imp (fun _ _ h => h) (fun _ _ _ _ _ ⟨h, he⟩ => ⟨h.trans rfl, he⟩) le_rfl le_rfl)
@@ -371,7 +366,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis
     (fun n hn => (hN (a n, (q n, mv n))).imp (fun _ _ h => h)
       (fun _ _ _ _ _ ⟨h, he⟩ => ⟨by rw [h]; simp [hq n hn, mv, st, peekWord, slot], he⟩) (by
         have := hP (a n) n hn.le (mv n); have := (hst n hn.le).1
-        have : (encPeek (encPair encS encMove) (none, (step (q n) (a n)).1,
+        have : (encPeek (encPair encS encSign) (none, (step (q n) (a n)).1,
             (step (q n) (a n)).2.1)).length ≤ 2 * L + 4 := by
           have := hP none (n + 1) hn (step (q n) (a n)).2.1
           rw [hq n hn] at this
@@ -384,7 +379,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis
               2 * Tm + 8 * L + 20 by omega)
         dsimp -zeta only; simp only [Function.comp_apply]; omega) (by
         have := hP (a n) n hn.le (mv n); have := (hst n hn.le).2
-        have : (encPeek (encPair encS encMove) (none, (step (q n) (a n)).1,
+        have : (encPeek (encPair encS encSign) (none, (step (q n) (a n)).1,
             (step (q n) (a n)).2.1)).length ≤ 2 * L + 4 := by
           have := hP none (n + 1) hn (step (q n) (a n)).2.1
           rw [hq n hn] at this
@@ -437,7 +432,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis
   -- the bounds
   have hround (n : ℕ) (hn : n < R) : stepRoundTime (stepFlagWord (!halt (q n))).length
       (peekWord (a n) ++ encAug encS (q n, mv n)).length
-      (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encMove (st n).2.1).length
+      (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encSign (st n).2.1).length
       (D * (Tm + 4 * L + 10) + 4) (D * (2 * Tm + 8 * L + 20) + 2 * L + 10) (D * (2 * L + 5) + 7)
       (D * (Tm + 2 * L + 5) + 7) + 1 ≤ 100 * (D * (Tm + L + 1)) := by
     have h₁ := hP (a n) n hn.le (mv n)
@@ -457,7 +452,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis
     omega
   have hS : ∑ n ∈ Finset.range R, (stepRoundTime (stepFlagWord (!halt (q n))).length
       (peekWord (a n) ++ encAug encS (q n, mv n)).length
-      (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encMove (st n).2.1).length
+      (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encSign (st n).2.1).length
       (D * (Tm + 4 * L + 10) + 4) (D * (2 * Tm + 8 * L + 20) + 2 * L + 10) (D * (2 * L + 5) + 7)
       (D * (Tm + 2 * L + 5) + 7) + 1) ≤ R * (100 * (D * (Tm + L + 1))) :=
     (Finset.sum_le_sum fun n hn => hround n (Finset.mem_range.mp hn)).trans (by simp)
@@ -495,7 +490,7 @@ public structure ResourceCertificate {σ : Type} (m : StepMachine σ Bool Bool)
     (T S : σ → ℕ) : Prop where
   computable_halt : ComputableInO m.halt encS encBool T S
   computable_step : ComputableInO (fun p : σ × Option Bool => m.step p.1 p.2)
-    (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits))
+    (encPair encS (encOption encBool)) (encPair encS (encPair encSign encBits))
     (fun p => T p.1) fun p => S p.1
 
 /-- The step machine `m` started in the state `s`. -/
@@ -535,7 +530,7 @@ public theorem ResourceCertificate.computableInBigO_of_init {σ γ ω : Type} {e
       rw [(m.withInit (init x)).run_succ_of_not_halt hh]
       have h₁ := hcS (((m.withInit (init x)).run (encIn x) i).state,
         inputSymbolAt (encIn x) ((m.withInit (init x)).run (encIn x) i).pos)
-      have h₂ := length_le_encPair_left encS (encPair encMove encBits)
+      have h₂ := length_le_encPair_left encS (encPair encSign encBits)
         (m.step ((m.withInit (init x)).run (encIn x) i).state
           (inputSymbolAt (encIn x) ((m.withInit (init x)).run (encIn x) i).pos))
       have h₃ := Nat.mul_le_mul_left cS (Nat.add_le_add_right (hmax x i (by omega)).2 1)
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean
index 0f5ac5e9a2..0d96f32218 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.IterateWhile
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Basic
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 import Complexity.Computability.Machines.Turing.MultiTape.Universal.Input
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
 import Mathlib.Tactic.Linarith
@@ -52,12 +53,6 @@ namespace Turing.MultiTapeTM.Universal
 
 /-! ### Encodings -/
 
-/-- Moves, by their sign. -/
-@[expose] public def encSign : SignType ↪ List Bool :=
-  ⟨fun m => match m with | .zero => [] | .neg => [false] | .pos => [true], by
-    intro a b h
-    cases a <;> cases b <;> simp_all⟩
-
 /-- Symbols and blanks. -/
 public abbrev eSym : Option ℕ ↪ List Bool := encOption encUnary
 
@@ -69,12 +64,6 @@ public abbrev eSym : Option ℕ ↪ List Bool := encOption encUnary
 /-- An action on a work tape. -/
 public abbrev TapeAct := Option (Option ℕ) × SignType
 
-/-- The unit type, encoded by the empty word. -/
-@[expose] public def encUnit : Unit ↪ List Bool := ⟨fun _ => [], fun _ _ _ => rfl⟩
-
-@[simp]
-public lemma encUnit_apply (u : Unit) : encUnit u = [] := rfl
-
 /-- Actions on a work tape. -/
 public abbrev eTA : Option (Option ℕ) × SignType ↪ List Bool := encPair (encOption eSym) encSign
 
@@ -250,12 +239,6 @@ lemma length_encList_eq_le (l : List (Option ℕ)) :
       (encList eSym l).length := by
   cases l <;> simp
 
-lemma length_encInt_add_one (z : ℤ) : (encInt (z + 1)).length ≤ (encInt z).length + 1 := by
-  rw [length_encInt, length_encInt]; split_ifs <;> omega
-
-lemma length_encInt_sub_one (z : ℤ) : (encInt (z - 1)).length ≤ (encInt z).length + 1 := by
-  rw [length_encInt, length_encInt]; split_ifs <;> omega
-
 /-- Applying an action at most doubles a work tape, up to the length of the action. -/
 lemma length_eTape_apply (t : Tape) (a : Option (Option ℕ) × SignType) :
     (eTape (t.apply a)).length ≤ 2 * (eTape t).length + 2 * (eTA a).length + 8 := by
@@ -263,8 +246,8 @@ lemma length_eTape_apply (t : Tape) (a : Option (Option ℕ) × SignType) :
   obtain ⟨w, m⟩ := a
   have := length_encList_eq_le l
   have := length_encList_eq_le r
-  have := length_encInt_add_one h
-  have := length_encInt_sub_one h
+  have := length_encInt_add_one_le h
+  have := length_encInt_sub_one_le h
   rcases w with _ | o <;> rcases m with _ | _ | _ <;>
     simp only [Tape.apply, Tape.move, Tape.write, Tape.read, Option.elim, eTape_apply,
       length_encPair, encList_cons, List.length_append, length_frame, encOption_some,
@@ -296,6 +279,16 @@ lemma length_read_le (t : Tape) : (eSym t.read).length ≤ (eTape t).length := b
   simp only [Tape.read, eTape_apply, length_encPair] at *
   omega
 
+/-- The symbols under the heads are no longer than the work tapes. -/
+lemma length_encList_map_read_le (ts : List Tape) :
+    (encList eSym (ts.map Tape.read)).length ≤ (encList eTape ts).length := by
+  induction ts with
+  | nil => simp
+  | cons t ts ih =>
+    have := length_read_le t
+    simp only [List.map_cons, encList_cons, List.length_append, length_frame] at *
+    omega
+
 /-! ### All work tapes -/
 
 open ComputableTidilyInO
@@ -350,19 +343,11 @@ public theorem reads_inO :
     ComputableTidilyInO (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
-  have hmap (ts : List Tape) : (encList eSym (ts.map fun t => t.read)).length ≤
-      (encList eTape ts).length := by
-    induction ts with
-    | nil => simp
-    | cons t ts ih =>
-      have := length_read_le t
-      simp only [List.map_cons, encList_cons, List.length_append, length_frame] at *
-      omega
   refine ((mapWith (encP := encUnit) (f := fun p : Unit × Tape => p.2.read)
     (read_deg.inO_one.comp_linear (snd encUnit eTape)) (const ())
     (of_linear (.of_eq fun _ => rfl))).mono 8 (fun ts => ?_) fun ts => ?_)
   all_goals
-    have h₁ := hmap ts
+    have h₁ : (encList eSym (ts.map fun t => t.read)).length ≤ _ := length_encList_map_read_le ts
     have h₂ : listMax (fun t => (encPair encUnit eTape ((), t)).length) ts ≤
         (encList eTape ts).length + 1 :=
       listMax_le fun t ht => by
@@ -464,29 +449,26 @@ lemma length_wTable_le :
     (encList (encPair eKey eAct) c.1.1.table).length ≤ (eWCtx c).length := by
   rw [length_eWCtx]; simp only [eDesc_apply, length_encPair]; omega
 
-lemma length_le_wTime {A B : ℕ}
-    (hA : A ≤ c.1.2.workTapes.length + c.1.1.table.length)
-    (hB : B ≤ (eWCtx c).length) :
-    (A + 1) * ((eDesc c.1.1).length + 1) * (B + 1) ≤ wTime c :=
-  (Nat.mul_le_mul (Nat.mul_le_mul_right _ (by omega)) (by omega)).trans
-    (Nat.le_add_right _ _)
-
-lemma length_le_wTime' {A B : ℕ}
+lemma length_le_wTime {A B k : ℕ}
     (hA : A ≤ c.1.2.workTapes.length + c.1.1.table.length)
-    (hB : B ≤ (eWCtx c).length) : (A + 1) * (B + 1) ≤ wTime c :=
-  (Nat.mul_le_mul_right (B + 1)
-    (Nat.le_mul_of_pos_right (A + 1) (Nat.succ_pos _))).trans
-      (length_le_wTime c hA hB)
+    (hB : B ≤ (eWCtx c).length) (hk : k ≤ (eDesc c.1.1).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) :
+    (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
+  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₂ : (encList eSym (c.1.2.workTapes.map Tape.read)).length ≤
-      (encList eTape c.1.2.workTapes).length := by
-    induction c.1.2.workTapes with
-    | nil => simp
-    | cons t ts ih =>
-      have := length_read_le t
-      simp only [List.map_cons, encList_cons, List.length_append, length_frame] at *
-      omega
+  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
   rw [length_eWCtx]
   simp only [wKey, eKey_apply, length_encPair, encUnary_apply, List.length_replicate]
@@ -513,7 +495,7 @@ abbrev WPart {β : Type} (f : WCtx → β) (enc : β ↪ List Bool) : Prop :=
   ComputableTidilyInO 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
+  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 :
@@ -533,9 +515,9 @@ public theorem stepWith_inO :
     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)
-      dsimp only [eWCtx, Function.comp_apply] at *
+      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
@@ -557,14 +539,6 @@ public theorem stepWith_inO :
       have hk := length_wKey_le c
       have ht := length_wTable_le c
       have hst := le_wTime c
-      have hentry (e : Key × Act) (he : e ∈ c.1.1.table) :
-          (encPair eKey eAct e).length ≤ (eWCtx c).length :=
-        (length_le_encList_of_mem (encPair eKey eAct) he).trans ht
-      have hentryD (e : Key × Act) (he : e ∈ c.1.1.table) :
-          (encPair eKey eAct e).length ≤ (eDesc c.1.1).length := by
-        have := length_le_encList_of_mem (encPair eKey eAct) he
-        simp only [eDesc_apply, length_encPair] at *
-        omega
       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
@@ -574,16 +548,16 @@ public theorem stepWith_inO :
             ((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₁ := hentry e he
+          have h₁ := length_le_of_mem_table c he
           have h₂ := length_le_encPair_left eKey eAct e
-          have hD := hentryD e he
+          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
+        (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))
@@ -597,7 +571,7 @@ public theorem stepWith_inO :
           (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₁ := hentry e he
+          have h₁ := length_le_of_mem_table c he
           have h₂ := length_le_encPair_left eKey eAct e
           simp only [length_encPair] at *
           omega
@@ -643,8 +617,9 @@ public theorem stepWith_inO :
         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)
-        (B := (eWCtx c).length) le_rfl
+      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
diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
index a09c432612..100ae21c74 100644
--- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
+++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
@@ -12,7 +12,7 @@ public import Complexity.Computability.Complexity.FineGrained.CountingSparsifica
 public import Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule
 public import Complexity.Computability.Complexity.FineGrained.SparseBranchAsymptotics
 public import Complexity.Computability.Complexity.FineGrained.SparseCountingScale
-public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 public import Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter
 public import Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime
@@ -79,7 +79,6 @@ open Cslib.Complexity.SubexponentialSAT Cslib.Complexity.SubexponentialSAT.Spars
 open Cslib.GenericRAM Cslib.GenericRAM.ExhaustiveCountFallback
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.ClauseSet.Sparsification
 open Turing.MultiTapeTM
-open Turing.MultiTapeTM.Universal (encUnit)
 
 local notation "encSys" => encList (encList (encList encNat))
 local notation "encLeafCtx" => encPair encUnit encUnary
diff --git a/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean b/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
index ff29b27977..6701ea1715 100644
--- a/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
+++ b/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
@@ -59,11 +59,11 @@ example : ∃ N₀_leaf N₀_top C_t d_t A_t : ℕ, 1 ≤ A_t ∧
     ∀ x : (Unit × ℕ) × Logic.PL.CNF ℕ, x.2.length ≤ leafOccBound 3 x.1.2 * x.1.2 + 1 →
       ((branchedSparseCNFDeclaredCertificate 3 N₀_leaf N₀_top 16384
           boundedIncidenceBranchCertificate branchBound16384).time x : ℝ) ≤
-        (C_t : ℝ) * ((encPair (encPair Universal.encUnit encUnary) encCNF x).length + 1 : ℝ) ^
+        (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^
           d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧
       ((branchedSparseCNFLeafCertificate 3 N₀_leaf N₀_top 16384
           boundedIncidenceBranchCertificate branchBound16384).time x : ℝ) ≤
-        (C_t : ℝ) * ((encPair (encPair Universal.encUnit encUnary) encCNF x).length + 1 : ℝ) ^
+        (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^
           d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) :=
   exists_branchedSparseCNF_time_bound 3 16384 boundedIncidenceBranchCertificate branchBound16384
     polyBounded_boundedIncidenceBranchCertificate_space
diff --git a/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
index c8e3427fc8..8185a562cb 100644
--- a/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
+++ b/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
@@ -20,7 +20,6 @@ open Cslib.Complexity Cslib.Complexity.BranchedSparseCNFCounter Cslib.GenericRAM
 open Cslib.Complexity.SparseCNFLeafCounter Cslib.Complexity.SubexponentialSAT
 open Cslib.Complexity.SubexponentialSAT.SparsePolyCounter Cslib.GenericRAM.ExhaustiveCountFallback
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM
-open Turing.MultiTapeTM.Universal (encUnit)
 
 local notation "encLeafIn" => encPair (encPair encUnit encUnary) encCNF
 
diff --git a/ComplexityTests/FiniteCSP.lean b/ComplexityTests/FiniteCSP.lean
index 30c200f5ff..d7429b5778 100644
--- a/ComplexityTests/FiniteCSP.lean
+++ b/ComplexityTests/FiniteCSP.lean
@@ -6,6 +6,7 @@ Authors: Samuel Schlesinger
 
 import Complexity.Logics.Propositional.CSP.ToBoolean
 import Complexity.Computability.Complexity.FineGrained.CountingFiniteCSP
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 
 /-!
 # Finite-domain CSP unit tests
@@ -101,10 +102,6 @@ example :
 example : (triangleCSP.toBoolean 3 3).numVars ≤ 3 * CSP.bitWidth 3 :=
   CSP.numVars_toBoolean_le (by decide)
 
-/-- Trivial encoding for the singleton relation alphabet `Unit`. -/
-def encUnit : Unit ↪ List Bool :=
-  ⟨fun _ => [], fun _ _ _ => rfl⟩
-
 -- Polynomial-time compilation and compiled encoding length bound
 example :
     ComputableInPolyTime (fun x : ℕ × CSP Unit ℕ => x.2.toBoolean 3 x.1)
diff --git a/ComplexityTests/Space/Savitch.lean b/ComplexityTests/Space/Savitch.lean
index 06c37d8d85..0a9571d591 100644
--- a/ComplexityTests/Space/Savitch.lean
+++ b/ComplexityTests/Space/Savitch.lean
@@ -6,7 +6,7 @@ Authors: Bolton Bailey, Samuel Schlesinger
 
 import Complexity.Algorithms.Reachability.Savitch
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Space.Reachability
-import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives
 
 /-!
@@ -22,7 +22,6 @@ polynomial-space form for a family of depths, so that their hypotheses are satis
 namespace ComplexityTests.Savitch
 
 open Cslib Cslib.Reachability Turing.MultiTapeTM
-open Turing.MultiTapeTM.Universal (encUnit)
 
 /-! ### The binary counter -/