chore(Machines): remove unreferenced tidy declarations (#862)

Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean

@@ -54,10 +54,6 @@ theorem weaken {f : α → β} (h : ComputableTidilyInSpace f encIn encB S) (hS
   let ⟨T, hT⟩ := h
   ⟨T, hT.weaken (.refl _) hS⟩
 
-theorem mono_le {f : α → β} (h : ComputableTidilyInSpace f encIn encB S)
-    (hS : ∀ a, S a ≤ S₁ a) : ComputableTidilyInSpace f encIn encB S₁ :=
-  h.weaken (.of_le hS)
-
 theorem length_le {f : α → β} (h : ComputableTidilyInSpace f encIn encB S) :
     (fun a => (encB (f a)).length) ≼ S :=
   let ⟨_, hT⟩ := h
@@ -68,12 +64,6 @@ theorem of_enc_eq {f : α → β} {g : α → γ} (h : ComputableTidilyInSpace f
   let ⟨T, hT⟩ := h
   ⟨T, hT.of_enc_eq he⟩
 
-theorem of_encIn_eq {α' : Type} {encIn' : α' ↪ List Bool} {f : α → β} (e : α' → α)
-    (h : ComputableTidilyInSpace f encIn encB S) (he : ∀ a, encIn' a = encIn (e a)) :
-    ComputableTidilyInSpace (fun a => f (e a)) encIn' encB fun a => S (e a) :=
-  let ⟨_, hT⟩ := h
-  ⟨_, hT.of_encIn_eq e he⟩
-
 theorem comp {f : α → β} {g : β → γ} {S₂ : β → ℕ} (hg : ComputableTidilyInSpace g encB encC S₂)
     (hf : ComputableTidilyInSpace f encIn encB S₁) :
     ComputableTidilyInSpace (fun a => g (f a)) encIn encC fun a => S₁ a + S₂ (f a) :=
@@ -89,14 +79,6 @@ theorem prod {f : α → β} {g : α → γ} (hf : ComputableTidilyInSpace f enc
   let ⟨_, hg⟩ := hg
   ⟨_, hf.prod hg⟩
 
-theorem append {f₁ : α → β} {f₂ : α → γ} {g : α → δ} {encD : δ ↪ List Bool}
-    (h₁ : ComputableTidilyInSpace f₁ encIn encB S₁) (h₂ : ComputableTidilyInSpace f₂ encIn encC S₂)
-    (hg : ∀ x, encD (g x) = encB (f₁ x) ++ encC (f₂ x)) :
-    ComputableTidilyInSpace g encIn encD fun x => S₁ x + S₂ x :=
-  let ⟨_, h₁⟩ := h₁
-  let ⟨_, h₂⟩ := h₂
-  ⟨_, h₁.append h₂ hg⟩
-
 theorem ite {c : α → Bool} {f g : α → β} {Sc : α → ℕ}
     (hc : ComputableTidilyInSpace c encIn encBool Sc) (hf : ComputableTidilyInSpace f encIn encB S₁)
     (hg : ComputableTidilyInSpace g encIn encB S₂) :

Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean

@@ -34,8 +34,6 @@ It also records the equivalence with `Turing.MultiTapeTM.ComputableTidilyInSpace
 * `Turing.MultiTapeTM.ComputableInSpace.comp`, `.prod`, `.append`, `.ite`: plain closure rules.
 * `Turing.MultiTapeTM.ComputableInSpace.iterate`, `.foldl`, `.foldlWith`: plain space-bounded
   loops.
-* `Turing.MultiTapeTM.computableInSpace_iff_computableTidilyInSpace`: equivalence with the tidy
-  counterpart.
 -/
 
 @[expose] public section
@@ -68,11 +66,6 @@ theorem ComputableTidilyInSpace.computableInSpace (h : ComputableTidilyInSpace f
     ComputableInSpace f encIn encOut S :=
   .of_tidy h
 
-/-- **Plain and tidy computability within a space bound agree.** -/
-theorem computableInSpace_iff_computableTidilyInSpace :
-    ComputableInSpace f encIn encOut S ↔ ComputableTidilyInSpace f encIn encOut S :=
-  ⟨ComputableInSpace.tidy, ComputableInSpace.of_tidy⟩
-
 end Bridge
 
 namespace ComputableInSpace

Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean

@@ -17,16 +17,13 @@ import Mathlib.Tactic.Linarith
 Operations on lists encoded by `Turing.MultiTapeTM.encList`, with explicit degrees
 (`Turing.MultiTapeTM.ComputableTidilyInDegree`): adding an element at either end and concatenation
 in linear time; finding the first element that passes a test and keeping the elements that pass a
-test, one degree above the test; and dropping a number of elements in quadratic time. The tests may
-depend on a parameter.
+test, one degree above the test. The tests may depend on a parameter.
 
 ## Main results
 
 * `Turing.MultiTapeTM.ComputableTidilyInDegree.cons`, `.snoc`, `.listAppend`.
 * `Turing.MultiTapeTM.ComputableTidilyInDegree.findWith`: the first element passing a test.
 * `Turing.MultiTapeTM.ComputableTidilyInDegree.filterWith`: the elements passing a test.
-* `Turing.MultiTapeTM.ComputableTidilyInDegree.dropUnary`: dropping a number of elements, given
-  in unary.
 -/
 
 namespace Turing.MultiTapeTM
@@ -182,29 +179,6 @@ public theorem filterWith {t : π × α → Bool} {par : γ → π} {list : γ 
   funext x
   rw [foldl_filterStep, List.nil_append]
 
-/-- Dropping the first `n` elements, with `n` in unary. -/
-public theorem dropUnary (enc : α ↪ List Bool) :
-    ComputableTidilyInDegree (fun p : List α × ℕ => p.1.drop p.2)
-      (encPair (encList enc) encUnary) (encList enc) 2 1 := by
-  have hrep (l : List α) (n : ℕ) : (List.replicate n true).foldl (fun acc _ => acc.tail) l =
-      l.drop n := by
-    simp [List.foldl_const, List.tail_iterate]
-  have hfold := foldl' (encA := encBool) (encL := encBits) (encB := encList enc)
-    (list := fun p : List α × ℕ => List.replicate p.2 true) (step := fun acc _ => acc.tail)
-    ((of_eq (f := fun n => List.replicate n true) (encIn := encUnary) (encMid := encBits)
-      fun _ => rfl).comp (snd (encList enc) encUnary))
-    (fst (encList enc) encUnary)
-    ((tail (enc₁ := enc)).comp (fst (encList enc) encBool))
-    (B := fun p => (encPair (encList enc) encUnary p).length) .self (fun p i hi => by
-      rw [List.take_replicate, hrep]
-      have := SizedListEncoding.length_drop_le (encA := enc) (encL := encList enc) p.1
-        (min i p.2)
-      simp only [length_encPair]
-      omega)
-  convert hfold.mono (d' := 2) (e' := 1) using 1
-  funext p
-  rw [hrep]
-
 /-- One step of mapping with the parameter `p`. -/
 @[expose] public def mapStep {β : Type} (f : π × α → β) (p : π) (acc : List β) (a : α) :
     List β :=
@@ -327,20 +301,6 @@ public theorem isSome (enc : α ↪ List Bool) :
   funext o
   cases o <;> rfl
 
-/-- The length of a list, in unary. -/
-public theorem length (enc : α ↪ List Bool) :
-    ComputableTidilyInDegree (fun l : List α => l.length) (encList enc) encUnary 2 1 := by
-  have hfold := foldl' (encL := encList enc) (encB := encUnary) (list := id)
-    (init := fun _ => 0) (step := fun n _ => n + 1) (of_eq fun _ => rfl) (const 0)
-    (unary_succ.comp (fst encUnary enc)) (B := fun l => (encList enc l).length) .self
-    (fun l i hi => by
-      have := length_le_length_encList enc l
-      simp [List.foldl_const]
-      omega)
-  convert hfold.mono (d' := 2) (e' := 1) using 1
-  funext l
-  simp [List.foldl_const]
-
 /-- A list of `n` copies of an element. -/
 public theorem replicate (enc : α ↪ List Bool) :
     ComputableTidilyInDegree (fun p : ℕ × α => List.replicate p.1 p.2) (encPair encUnary enc)

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean

@@ -21,12 +21,9 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Ba
 `Turing.MultiTapeTM.ComputableTidilyInPolySpace f encIn encOut`: `f` is tidily computable
 (`Turing.MultiTapeTM.ComputableTidilyInO`) within some time and within space polynomially bounded in
 the length of the encoded input. Unlike `Turing.MultiTapeTM.ComputableTidilyInPolyTime`, no bound on
-the time is imposed, so the notion is closed under iterating a step an exponential number of times,
-counted in binary, as long as the states stay of polynomial size
-(`Turing.MultiTapeTM.ComputableTidilyInPolySpace.iterate`). It is also closed under composition,
-pairing and case distinction, and contains polynomial time; these closure properties are registered
-with `fun_prop`. A Boolean function computable within polynomial space decides a problem in `PSPACE`
-(`Cslib.Complexity.mem_PSPACE_iff_computableInPolySpace`).
+the time is imposed. It contains polynomial time. The closure rules (composition, pairing, case
+distinction and binary-counted iteration) are stated for the plain predicate
+`Turing.MultiTapeTM.ComputableInPolySpace`.
 
 Exhaustive searches within polynomial space enumerate their candidates with the binary counter
 `Cslib.BitString.increment`, which is computable in linear time
@@ -40,8 +37,6 @@ Exhaustive searches within polynomial space enumerate their candidates with the
 
 * `Turing.MultiTapeTM.ComputableTidilyInPolySpace.of_polyTime`: polynomial time is within
   polynomial space.
-* `Turing.MultiTapeTM.ComputableTidilyInPolySpace.comp`, `.prod`, `.ite`: closure properties.
-* `Turing.MultiTapeTM.ComputableTidilyInPolySpace.iterate`: iteration within polynomial space.
 * `Turing.MultiTapeTM.ComputableTidilyInDegree.increment`: the binary counter in linear time.
 -/
 
@@ -57,8 +52,7 @@ def ComputableTidilyInPolySpace {α β : Type} (f : α → β) (encIn : α ↪ L
 
 namespace ComputableTidilyInPolySpace
 
-variable {α β γ δ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool}
-  {encOut : γ ↪ List Bool} {encD : δ ↪ List Bool}
+variable {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool}
 
 /-- **Polynomial time is within polynomial space.** -/
 theorem of_polyTime {f : α → β} (h : ComputableTidilyInPolyTime f encIn encMid) :
@@ -67,89 +61,9 @@ theorem of_polyTime {f : α → β} (h : ComputableTidilyInPolyTime f encIn encM
   exact ⟨_, _, PolyBounded.of_forall_le (u := fun a => ((encIn a).length + 1) ^ d) 1 d
     fun a => by simp, h.inO⟩
 
-/-- The encoded values have polynomial length. -/
-theorem polyBounded_length {f : α → β} (h : ComputableTidilyInPolySpace f encIn encMid) :
-    PolyBounded (fun a => (encIn a).length) fun a => (encMid (f a)).length := by
-  obtain ⟨T, S, hS, h⟩ := h
-  obtain ⟨c, hc⟩ := h.length_le
-  exact ((PolyBounded.const c).mul (hS.add (.const 1))).mono hc
-
-/-- Composition. -/
-theorem comp {f : β → γ} {g : α → β} (hf : ComputableTidilyInPolySpace f encMid encOut)
-    (hg : ComputableTidilyInPolySpace g encIn encMid) :
-    ComputableTidilyInPolySpace (fun a => f (g a)) encIn encOut := by
-  have hlen := hg.polyBounded_length
-  obtain ⟨Tf, Sf, hSf, hf'⟩ := hf
-  obtain ⟨Tg, Sg, hSg, hg'⟩ := hg
-  exact ⟨_, _, hSg.add (hSf.comp hlen), hf'.comp hg'⟩
-
-/-- The identity. -/
-theorem id' : ComputableTidilyInPolySpace (fun a : α => a) encIn encIn :=
-  of_polyTime ComputableTidilyInPolyTime.id'
-
-/-- Pairing. -/
-theorem prod {f : α → β} {g : α → δ} (hf : ComputableTidilyInPolySpace f encIn encMid)
-    (hg : ComputableTidilyInPolySpace g encIn encD) :
-    ComputableTidilyInPolySpace (fun a => (f a, g a)) encIn (encPair encMid encD) := by
-  obtain ⟨Tf, Sf, hSf, hf⟩ := hf
-  obtain ⟨Tg, Sg, hSg, hg⟩ := hg
-  exact ⟨_, _, hSf.add hSg, hf.prod hg⟩
-
-/-- Case distinction. -/
-theorem ite {c : α → Bool} {f g : α → β} (hc : ComputableTidilyInPolySpace c encIn encBool)
-    (hf : ComputableTidilyInPolySpace f encIn encMid)
-    (hg : ComputableTidilyInPolySpace g encIn encMid) :
-    ComputableTidilyInPolySpace (fun a => if c a then f a else g a) encIn encMid := by
-  obtain ⟨Tc, Sc, hSc, hc⟩ := hc
-  obtain ⟨Tf, Sf, hSf, hf⟩ := hf
-  obtain ⟨Tg, Sg, hSg, hg⟩ := hg
-  refine ⟨_, _, (hSc.add (hSf.add hSg)).mono fun a => ?_, hc.ite hf hg⟩
-  split_ifs <;> lia
-
-/-- Agreement with a function computable within polynomial space. -/
-theorem congr {f g : α → β} (h : ComputableTidilyInPolySpace f encIn encMid)
-    (hfg : ∀ a, f a = g a) : ComputableTidilyInPolySpace g encIn encMid := by
-  rwa [show g = f from funext fun a => (hfg a).symm]
-
-/-- **Iteration within polynomial space**: iterating a step computable within polynomial space a
-number of times computed in polynomial time in binary, from a start computable within polynomial
-space, is within polynomial space when all the states along the way have polynomial length. -/
-theorem iterate [Inhabited β] {n : α → ℕ} {init : α → β} {step : β → β}
-    (hn : ComputableTidilyInPolyTime n encIn encNat)
-    (hinit : ComputableTidilyInPolySpace init encIn encMid)
-    (hstep : ComputableTidilyInPolySpace step encMid encMid) {B : α → ℕ}
-    (hB : PolyBounded (fun a => (encIn a).length) B)
-    (hstate : ∀ a, ∀ k ≤ n a, (encMid (step^[k] (init a))).length ≤ B a) :
-    ComputableTidilyInPolySpace (fun a => step^[n a] (init a)) encIn encMid := by
-  obtain ⟨dn, _, hn'⟩ := hn.exists_degree
-  obtain ⟨Ti, Si, hSi, hinit⟩ := hinit
-  obtain ⟨Ts, Ss, hSs, hstep⟩ := hstep
-  obtain ⟨cs, ds, hSs⟩ := hSs.exists_le
-  have hit := (ComputableInO.iterate hn'.inO.computableInO hinit.computableInO hstep.computableInO
-    (R := fun a => (Finset.range (n a + 1)).sup fun k => Ts (step^[k] (init a)))
-    (Q := fun a => cs * (B a + 1) ^ ds) (B := B)
-    (fun a k hk => Finset.le_sup (f := fun k => Ts (step^[k] (init a)))
-      (Finset.mem_range.mpr (Nat.lt_succ_of_le hk)))
-    (fun a k hk => (hSs _).trans (Nat.mul_le_mul_left cs
-      (Nat.pow_le_pow_left (Nat.add_le_add_right (hstate a k hk) 1) ds)))
-    hstate).tidy
-  refine ⟨_, _, ?_, hit⟩
-  have hQ : PolyBounded (fun a => (encIn a).length) fun a => cs * (B a + 1) ^ ds :=
-    PolyBounded.comp (size' := id) (v := fun m => cs * (m + 1) ^ ds)
-      (PolyBounded.of_forall_le cs ds fun _ => le_rfl) hB
-  exact ((((PolyBounded.of_forall_le (u := fun a => ((encIn a).length + 1) ^ dn) 1 dn
-    fun a => by simp).add hSi).add hQ).add hB).add hn.polyBounded_length
-
 /-! ### Automation -/
 
-attribute [fun_prop] ComputableTidilyInPolySpace of_polyTime id' prod ite
-
-/-- Composition, in the form used by `fun_prop`. -/
-@[fun_prop]
-theorem comp' {f : β → γ} {g : α → β} (hf : ComputableTidilyInPolySpace f encMid encOut)
-    (hg : ComputableTidilyInPolySpace g encIn encMid) :
-    ComputableTidilyInPolySpace (fun a => f (g a)) encIn encOut :=
-  hf.comp hg
+attribute [fun_prop] ComputableTidilyInPolySpace of_polyTime
 
 end ComputableTidilyInPolySpace
 

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean

@@ -19,9 +19,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormal
 
 `ComputableTidilyInPolyTime f encIn encOut`: `f` is tidily computable within time and space
 bounded by a polynomial in the length of the encoded input. The class is closed under composition,
-case distinctions and pairing, contains every function tidily computable in linear time and space,
-and does not depend on the encodings up to polynomial-time conversions
-(`Turing.MultiTapeTM.EncodingEquiv`).
+case distinctions and pairing, and contains every function tidily computable in linear time and
+space.
 
 ## Main definitions
 
@@ -34,10 +33,6 @@ and does not depend on the encodings up to polynomial-time conversions
 * `Turing.MultiTapeTM.PolyBounded.exists_le`, `.of_forall_le`: recover and supply explicit
   polynomial bounds for the size adapter over `Cslib.PolynomiallyBounded`.
 * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp`, `.ite`, `.pair`: closure properties.
-* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl`: left folds with polynomially bounded
-  intermediate states.
-* `Turing.MultiTapeTM.EncodingEquiv.computableTidilyInPolyTime_iff`: polynomial-time computability
-  transfers along equivalent encodings.
 * `Turing.MultiTapeTM.computableTidilyInPolyTime_succ`: the successor in binary.
 
 The closure properties are registered with `fun_prop`, so polynomial-time computability of a
@@ -228,60 +223,8 @@ public theorem trans (h₁₂ : EncodingEquiv enc₁ enc₂) (h₂₃ : Encoding
     EncodingEquiv enc₁ enc₃ :=
   ⟨h₂₃.1.comp h₁₂.1, h₁₂.2.comp h₂₃.2⟩
 
-/-- Polynomial-time computability does not depend on the encodings, up to equivalence. -/
-public theorem computableTidilyInPolyTime_iff {encIn encIn' : α ↪ List Bool}
-    {encOut encOut' : β ↪ List Bool} (hIn : EncodingEquiv encIn encIn')
-    (hOut : EncodingEquiv encOut encOut') {f : α → β} :
-    ComputableTidilyInPolyTime f encIn encOut ↔ ComputableTidilyInPolyTime f encIn' encOut' :=
-  ⟨fun h => (hOut.1.comp h).comp hIn.2, fun h => (hOut.2.comp h).comp hIn.1⟩
-
 end EncodingEquiv
 
-/-! ### Left folds -/
-
-/-- Left folds are tidily computable in polynomial time if the list, the initial value and `step`
-are, and the length of the list, the intermediate states and the arguments of `step` are bounded by
-a polynomial in the length of the encoded input. -/
-public theorem ComputableTidilyInPolyTime.foldl {γ α β : Type u} {encIn : γ ↪ List Bool}
-    {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool}
-    {encBA : β × α ↪ List Bool} {encS : List α × β ↪ List Bool}
-    {encO : Option (List α × β) ↪ List Bool}
-    [ListEncoding encA encL] [PairEncoding encB encA encBA] [PairEncoding encL encB encS]
-    [OptionEncoding encS encO] {list : γ → List α} {init : γ → β} {step : β → α → β}
-    (hlist : ComputableTidilyInPolyTime list encIn encL)
-    (hinit : ComputableTidilyInPolyTime init encIn encB)
-    (hstep : ComputableTidilyInPolyTime (fun p : β × α => step p.1 p.2) encBA encB)
-    {lMax aMax : γ → ℕ} (hlMax' : PolyBounded (fun x => (encIn x).length) lMax)
-    (haMax' : PolyBounded (fun x => (encIn x).length) aMax)
-    (hlen : PolyBounded (fun x => (encIn x).length) fun x => (list x).length)
-    (haMax : ∀ x i (hi : i < (list x).length),
-      (encBA (((list x).take i).foldl step (init x), (list x)[i])).length ≤ aMax x)
-    (hlMax : ∀ x, ∀ i ≤ (list x).length,
-      (encS ((list x).drop i, ((list x).take i).foldl step (init x))).length ≤ lMax x) :
-    ComputableTidilyInPolyTime (fun x => (list x).foldl step (init x)) encIn encB := by
-  obtain ⟨t₁, s₁, ht₁, hs₁, h₁⟩ := hlist
-  obtain ⟨t₂, s₂, ht₂, hs₂, h₂⟩ := hinit
-  obtain ⟨tS, sS, htS, hsS, hS⟩ := hstep
-  obtain ⟨ct, dt, htS⟩ := htS.exists_le
-  obtain ⟨cs, ds, hsS⟩ := hsS.exists_le
-  have hmax {c d : ℕ} : PolyBounded (fun x => (encIn x).length) fun x => c * (aMax x + 1) ^ d :=
-    PolyBounded.comp (size' := id) (v := fun n => c * (n + 1) ^ d)
-      (.of_forall_le c d (fun _ => le_rfl)) haMax'
-  obtain ⟨c, h⟩ := ComputableTidilyInTimeAndSpace.foldl (encA := encA) (encL := encL)
-    (encBA := encBA) (encS := encS) (encO := encO)
-    (h₁.mono (t' := fun x => t₁ x + t₂ x) (s' := fun x => s₁ x + s₂ x)
-      (fun _ => Nat.le_add_right _ _) (fun _ => Nat.le_add_right _ _))
-    (h₂.mono (fun _ => Nat.le_add_left _ _) (fun _ => Nat.le_add_left _ _)) hS
-    (tMax := fun x => ct * (aMax x + 1) ^ dt) (sMax := fun x => cs * (aMax x + 1) ^ ds)
-    (fun x i hi => (htS _).trans (Nat.mul_le_mul_left ct (Nat.pow_le_pow_left
-      (Nat.add_le_add_right (haMax x i hi) 1) dt)))
-    (fun x i hi => (hsS _).trans (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left
-      (Nat.add_le_add_right (haMax x i hi) 1) ds)))
-    hlMax
-  exact ⟨_, _, (PolyBounded.const c).mul ((ht₁.add ht₂).add
-      ((hlen.add (.const 1)).mul ((hmax.add hlMax').add (.const 1)))),
-    (PolyBounded.const c).mul ((((hs₁.add hs₂).add hmax).add hlMax').add (.const 1)), h⟩
-
 /-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`, from
 the transducer certificate `computableInTimeAndSpace_succ`. -/
 @[fun_prop]

Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean

@@ -29,7 +29,7 @@ into the tidy normal form
 (`Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace`), whose
 machines compose. Functions computable within bounds in the senses of
 `Turing.MultiTapeTM.ComputableInTimeAndSpace`, `Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace`,
-`Turing.MultiTapeTM.ComputableTidilyInO`, `Turing.MultiTapeTM.ComputableTidilyInDegree` and
+`Turing.MultiTapeTM.ComputableTidilyInDegree` and
 `Turing.MultiTapeTM.ComputableTidilyInPolyTime` are computable (their `.isComputable` lemmas), and
 decidable sets are closed under complement.
 
@@ -74,12 +74,6 @@ theorem ComputableTidilyInTimeAndSpace.isComputable {f : α → β} {t s : α 
     (h : ComputableTidilyInTimeAndSpace f encIn encMid t s) : IsComputable f encIn encMid :=
   h.computableInTimeAndSpace.isComputable
 
-/-- Functions tidily computable up to constants are computable. -/
-theorem ComputableTidilyInO.isComputable {f : α → β} {T S : α → ℕ}
-    (h : ComputableTidilyInO f encIn encMid T S) : IsComputable f encIn encMid :=
-  let ⟨_, h, _⟩ := h
-  h.isComputable
-
 /-- Functions tidily computable within bounds of given degrees are computable. -/
 theorem ComputableTidilyInDegree.isComputable {f : α → β} {d e : ℕ}
     (h : ComputableTidilyInDegree f encIn encMid d e) : IsComputable f encIn encMid :=