From ea97f8c5c16cc009928e2bf3527a9e0ed3d187ed Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sat, 31 Oct 2026 10:15:35 +0000 Subject: [PATCH] refactor(machines): retire superseded tidy list combinators Reuse the plain InO map rule for the unchanged space-only mapping bound, remove four superseded tidy declarations, and test captured-parameter mapping including empty lists. Lower the two baseline entries from freshly compiled module metadata. Focused strict builds, hygiene and aggregate checks pass; full hosted validation required. AI-assisted with Codex; independent review recorded on the PR. --- .../Turing/MultiTape/Complexity/BigO.lean | 206 +----------------- .../MultiTape/Complexity/BigO/Lists.lean | 7 +- .../MultiTape/Complexity/InSpaceLib.lean | 57 +---- ComplexityTests/InSpacePlain.lean | 21 ++ scripts/tidy_surface_baseline.json | 4 +- 5 files changed, 33 insertions(+), 262 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean index 8e6718beae..d91b4e8a62 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean @@ -7,6 +7,7 @@ Authors: Christian Reitwiessner module -- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted) -- vendored: use core's fold homomorphism law for the captured-parameter identity. +-- vendored: retire superseded tidy list combinators; plain rules live in BigO/Lists. public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Bounds public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds @@ -39,9 +40,7 @@ space. The encoded value counts towards the space since a combinator keeps it on ## Main results * `Turing.MultiTapeTM.ComputableTidilyInO.comp`, `.ite`, `.prod`: closure properties. -* `Turing.MultiTapeTM.ComputableTidilyInO.foldl`, `.foldlWith`: left folds. -* `Turing.MultiTapeTM.ComputableTidilyInO.findWith`, `.filterWith`, `.mapWith`: list operations - with a parameter. +* `Turing.MultiTapeTM.ComputableTidilyInO.foldl`, `.foldlWith`: left folds with a parameter. * `Turing.MultiTapeTM.ComputableTidilyInDegree.inO`: bounds of a given degree. -/ @@ -367,207 +366,6 @@ public theorem foldlWith [ListEncoding encA encL] [hS : SizedListEncoding encA e end Fold -/-! ### Finding, filtering and mapping -/ - -section Lists - -open ComputableTidilyInDegree (findStep foldl_findStep filterStep foldl_filterStep mapStep - foldl_mapStep length_encList_filter_le isSome optionSome snoc) - -variable {γ α β π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} {encB : β ↪ List Bool} - {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} - -/-- The first element of `list x` passing the test `t` with the parameter `par x`. -/ -public theorem findWith {t : π × α → Bool} {Tt St : π × α → ℕ} - (ht : ComputableTidilyInO t (encPair encP enc) encBool Tt St) - (hpar : ComputableTidilyInO par encIn encP Tp Sp) - (hlist : ComputableTidilyInO list encIn (encList enc) Tl Sl) : - ComputableTidilyInO (fun x => (list x).find? fun a => t (par x, a)) encIn (encOption enc) - (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * - ((encP (par x)).length + (encList enc (list x)).length + - listMax (fun a => Tt (par x, a)) (list x))) - fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + - (encList enc (list x)).length + listMax (fun a => St (par x, a)) (list x) := by - -- the step, as a function of `((p, acc), a)` - have hq := fst (encPair encP (encOption enc)) enc - have hel := snd (encPair encP (encOption enc)) enc - have hisSome := (isSome enc).inO_one.comp_linear hq.snd' - have h := hisSome.ite hq.snd' ((ht.comp (hq.fst'.prod hel)).ite - ((optionSome (enc₁ := enc)).inO_one.comp_linear hel) (const none)) - have hstep : ComputableTidilyInO (fun q : (π × Option α) × α => findStep t q.1.1 q.1.2 q.2) - (encPair (encPair encP (encOption enc)) enc) (encOption enc) - (fun q => (encPair (encPair encP (encOption enc)) enc q).length + Tt (q.1.1, q.2)) - fun q => (encPair (encPair encP (encOption enc)) enc q).length + St (q.1.1, q.2) := by - refine (h.mono 4 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨⟨p, acc⟩, a⟩ => ?_ - · split_ifs <;> omega - · split_ifs <;> omega - · cases acc <;> simp [findStep] - have hst (x : γ) (i : ℕ) : - (encOption enc (((list x).take i).foldl (findStep t (par x)) none)).length ≤ - (encList enc (list x)).length + 1 := by - rw [foldl_findStep, Option.none_or] - exact (length_encOption_find?_le enc _ _).trans - (Nat.add_le_add_right (length_encList_take_le enc _ _) 1) - have hfold := foldlWith (encL := encList enc) (encB := encOption enc) hpar hlist - (const none) hstep (R := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => Tt (par x, a)) (list x)) - (Q := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => St (par x, a)) (list x)) - (B := fun x => (encList enc (list x)).length + 1) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Tt (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => St (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by have := hst x i; omega) - refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ - · have h₁ := length_le_length_encList enc (list x) - have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by - rcases Nat.eq_zero_or_pos (list x).length with h | h - · simp [h] - · exact Nat.le_mul_of_pos_right _ (by omega) - ring_nf - omega - · omega - · rw [foldl_findStep, Option.none_or] - -/-- The elements of `list x` passing the test `t` with the parameter `par x`. -/ -public theorem filterWith {t : π × α → Bool} {Tt St : π × α → ℕ} - (ht : ComputableTidilyInO t (encPair encP enc) encBool Tt St) - (hpar : ComputableTidilyInO par encIn encP Tp Sp) - (hlist : ComputableTidilyInO list encIn (encList enc) Tl Sl) : - ComputableTidilyInO (fun x => (list x).filter fun a => t (par x, a)) encIn (encList enc) - (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * - ((encP (par x)).length + (encList enc (list x)).length + - listMax (fun a => Tt (par x, a)) (list x))) - fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + - (encList enc (list x)).length + listMax (fun a => St (par x, a)) (list x) := by - have hq := fst (encPair encP (encList enc)) enc - have hel := snd (encPair encP (encList enc)) enc - have h := (ht.comp (hq.fst'.prod hel)).ite - ((snoc enc).inO_one.comp_linear (hq.snd'.prod hel)) hq.snd' - have hstep : ComputableTidilyInO - (fun q : (π × List α) × α => filterStep t q.1.1 q.1.2 q.2) - (encPair (encPair encP (encList enc)) enc) (encList enc) - (fun q => (encPair (encPair encP (encList enc)) enc q).length + Tt (q.1.1, q.2)) - fun q => (encPair (encPair encP (encList enc)) enc q).length + St (q.1.1, q.2) := by - refine (h.mono 4 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨⟨p, acc⟩, a⟩ => ?_ - · split_ifs <;> omega - · split_ifs <;> omega - · simp [filterStep] - have hst (x : γ) (i : ℕ) : - (encList enc (((list x).take i).foldl (filterStep t (par x)) [])).length ≤ - (encList enc (list x)).length := by - rw [foldl_filterStep, List.nil_append] - exact (length_encList_filter_le enc _ _).trans (length_encList_take_le enc _ _) - have hfold := foldlWith (encL := encList enc) (encB := encList enc) hpar hlist - (const []) hstep (R := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => Tt (par x, a)) (list x)) - (Q := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => St (par x, a)) (list x)) - (B := fun x => (encList enc (list x)).length + 1) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Tt (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => St (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by have := hst x i; omega) - refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ - · have h₁ := length_le_length_encList enc (list x) - have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by - rcases Nat.eq_zero_or_pos (list x).length with h | h - · simp [h] - · exact Nat.le_mul_of_pos_right _ (by omega) - ring_nf - omega - · omega - · rw [foldl_filterStep, List.nil_append] - -/-- Mapping `f` with the parameter `par x` over `list x`. -/ -public theorem mapWith {f : π × α → β} {Tf Sf : π × α → ℕ} - (hf : ComputableTidilyInO f (encPair encP enc) encB Tf Sf) - (hpar : ComputableTidilyInO par encIn encP Tp Sp) - (hlist : ComputableTidilyInO list encIn (encList enc) Tl Sl) : - ComputableTidilyInO (fun x => (list x).map fun a => f (par x, a)) encIn (encList encB) - (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * - ((encP (par x)).length + (encList enc (list x)).length + - (encList encB ((list x).map fun a => f (par x, a))).length + - listMax (fun a => Tf (par x, a)) (list x))) - fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + - (encList enc (list x)).length + - (encList encB ((list x).map fun a => f (par x, a))).length + - listMax (fun a => Sf (par x, a)) (list x) := by - have hq := fst (encPair encP (encList encB)) enc - have hel := snd (encPair encP (encList encB)) enc - have h := (snoc encB).inO_one.comp (hq.snd'.prod (hf.comp (hq.fst'.prod hel))) - obtain ⟨c, hc⟩ := hf.length_le - obtain ⟨d, hd⟩ := hf.length_le_time - have hstep : ComputableTidilyInO (fun q : (π × List β) × α => mapStep f q.1.1 q.1.2 q.2) - (encPair (encPair encP (encList encB)) enc) (encList encB) - (fun q => (encPair (encPair encP (encList encB)) enc q).length + Tf (q.1.1, q.2)) - fun q => (encPair (encPair encP (encList encB)) enc q).length + Sf (q.1.1, q.2) := - h.mono (2 * c + 2 * d + 6) (fun q => by - have := hd (q.1.1, q.2) - simp only [length_encPair, Function.comp_apply] at this ⊢ - nlinarith) fun q => by - have := hc (q.1.1, q.2) - simp only [length_encPair, Function.comp_apply] at this ⊢ - nlinarith - have hst (x : γ) (i : ℕ) : - (encList encB (((list x).take i).foldl (mapStep f (par x)) [])).length ≤ - (encList encB ((list x).map fun a => f (par x, a))).length := by - rw [foldl_mapStep, List.nil_append, List.map_take] - exact length_encList_take_le encB _ _ - have hfold := foldlWith (encL := encList enc) (encB := encList encB) hpar hlist - (const []) hstep (R := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + - 3 * (encList encB ((list x).map fun a => f (par x, a))).length + 5 + - listMax (fun a => Tf (par x, a)) (list x)) - (Q := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + - 3 * (encList encB ((list x).map fun a => f (par x, a))).length + 5 + - listMax (fun a => Sf (par x, a)) (list x)) - (B := fun x => (encList encB ((list x).map fun a => f (par x, a))).length) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Tf (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Sf (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by have := hst x i; omega) - refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ - · have h₁ := length_le_length_encList enc (list x) - have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by - rcases Nat.eq_zero_or_pos (list x).length with h | h - · simp [h] - · exact Nat.le_mul_of_pos_right _ (by omega) - ring_nf - omega - · omega - · rw [foldl_mapStep, List.nil_append] - -end Lists - end ComputableTidilyInO end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean index e06cf3bb9f..a0d6727565 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean @@ -15,8 +15,7 @@ import Mathlib.Tactic.Ring /-! # Finding, filtering and mapping with parameters -Plain counterparts of `Turing.MultiTapeTM.ComputableTidilyInO.findWith`, `.filterWith` and -`.mapWith`: one left fold over `list x` whose step applies a test or function to the parameter +One left fold over `list x` applies a test or function to the parameter `par x` and the current element. The time bound charges each round for the parameter, the list, the accumulator and the largest cost of the test or function on an element. @@ -28,8 +27,8 @@ the accumulator and the largest cost of the test or function on an element. ## References -Restates Christian Reitwiessner's tidy list combinators -(`Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean`) in the plain calculus. +Derived from Christian Reitwiessner's original list-combinator construction, using the plain +fold rules and independent time and workspace bounds. -/ public section diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean index 1483300f0d..2bae8cadca 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpace.Plain public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives @@ -511,43 +512,10 @@ theorem mapWith {π κ : Type} {encP : π ↪ List Bool} {encK : κ ↪ List Boo (encList enc (list x)).length + (encList encK ((list x).map fun a => f (par x, a))).length + listMax (fun a => Sf (par x, a)) (list x) := by - have hfold_eq (p : π) (l : List ε) (acc : List κ) : - l.foldl (fun acc a => acc ++ [f (p, a)]) acc = acc ++ l.map (fun a => f (p, a)) := by - induction l generalizing acc with - | nil => simp - | cons a l ih => simp [ih, List.append_assoc] - have hq := fst (encPair encP (encList encK)) enc - have hel := snd (encPair encP (encList encK)) enc - obtain ⟨c, hc⟩ := hf.length_le - have hstep : ComputableInSpace (fun q : (π × List κ) × ε => q.1.2 ++ [f (q.1.1, q.2)]) - (encPair (encPair encP (encList encK)) enc) (encList encK) - fun q => (encPair (encPair encP (encList encK)) enc q).length + Sf (q.1.1, q.2) := - ((snoc encK).comp ((snd' hq).prod (hf.comp ((fst' hq).prod hel)))).weaken - ⟨2 * c + 6, fun q => by - have := hc (q.1.1, q.2) - simp only [length_encPair] at this ⊢ - nlinarith⟩ - have hst (x : α) (i : ℕ) : - (encList encK (((list x).take i).foldl (fun acc a => acc ++ [f (par x, a)]) [])).length ≤ - (encList encK ((list x).map fun a => f (par x, a))).length := by - rw [hfold_eq, List.nil_append, List.map_take] - exact length_encList_take_le encK _ _ - have hfold := foldlWith (encL := encList enc) (encB := encList encK) - (step := fun p acc a => acc ++ [f (p, a)]) hpar hlist (const []) hstep - (Q := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + - 3 * (encList encK ((list x).map fun a => f (par x, a))).length + 5 + - listMax (fun a => Sf (par x, a)) (list x)) - (B := fun x => (encList encK ((list x).map fun a => f (par x, a))).length) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Sf (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i _ => hst x i) - refine (hfold.weaken ⟨6, fun x => by dsimp only; omega⟩).of_enc_eq fun x => ?_ - rw [hfold_eq, List.nil_append] + obtain ⟨_, hf⟩ := hf.exists_inO + obtain ⟨_, hpar⟩ := hpar.exists_inO + obtain ⟨_, hlist⟩ := hlist.exists_inO + exact of_inO (ComputableInO.mapWith hf hpar hlist) end Generic @@ -872,21 +840,6 @@ theorem length : fun l => 8 * ((encList enc l).length + 1) := ComputableInSpace.length.tidy -theorem mapWith {π κ : Type} {encP : π ↪ List Bool} {encK : κ ↪ List Bool} {f : π × ε → κ} - {Sf : π × ε → ℕ} {par : α → π} {list : α → List ε} {Sp Sl : α → ℕ} - (hf : ComputableTidilyInSpace f (encPair encP enc) encK Sf) - (hpar : ComputableTidilyInSpace par encIn encP Sp) - (hlist : ComputableTidilyInSpace list encIn (encList enc) Sl) : - ComputableTidilyInSpace (fun x => (list x).map fun a => f (par x, a)) encIn (encList encK) - fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + - (encList enc (list x)).length + - (encList encK ((list x).map fun a => f (par x, a))).length + - listMax (fun a => Sf (par x, a)) (list x) := - let ⟨_, hf⟩ := hf - let ⟨_, hpar⟩ := hpar - let ⟨_, hlist⟩ := hlist - ⟨_, ComputableTidilyInO.mapWith hf hpar hlist⟩ - end Generic section BudgetOps diff --git a/ComplexityTests/InSpacePlain.lean b/ComplexityTests/InSpacePlain.lean index 1bde3ff441..d271d6cdde 100644 --- a/ComplexityTests/InSpacePlain.lean +++ b/ComplexityTests/InSpacePlain.lean @@ -114,4 +114,25 @@ theorem countUp_polySpace : ComputableInPolySpace countUp encNat encNat := by example (n : ℕ) : countUp n = n := by simp [countUp, ComputableInO.iterate_succ_eq] +/-- Mapping may use a captured parameter; the resulting list remains charged to space. -/ +def fill (p : Bool × List Bool) : List Bool := p.2.map fun _ => p.1 + +theorem fill_inSpace : + ComputableInSpace fill (encPair encBool (encList encBool)) (encList encBool) + fun p => 8 * ((encPair encBool (encList encBool) p).length + 1) := by + have hlen (xs : List Bool) : (encList encBool xs).length = 3 * xs.length := by + simp [length_encList, encBool_apply, Nat.mul_comm] + apply (ComputableInSpace.mapWith (ComputableInSpace.fst encBool encBool) + (ComputableInSpace.fst encBool (encList encBool)) + (ComputableInSpace.snd encBool (encList encBool))).mono_le + intro p + have hmax : listMax (fun a : Bool => (encPair encBool encBool (p.1, a)).length) p.2 ≤ 5 := + listMax_le fun a _ => by simp [encBool_apply] + simp only [length_encPair, encBool_apply, List.length_singleton, hlen, List.length_map] at hmax ⊢ + omega + +example : fill (true, [false, true, false]) = [true, true, true] := rfl +example : fill (false, [true, false]) = [false, false] := rfl +example : fill (true, []) = [] := rfl + end ComplexityTests.InSpacePlain diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 68e3022061..7dfe53675d 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -2,14 +2,14 @@ "Complexity/Computability/Machines/ReadMachine/Tidy.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Combinators/Encoding.lean": 8, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 32, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 29, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Plain.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree.lean": 24, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Fold.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 16, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 3, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 44, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 12, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean": 11,