From 619ca405def88a19c55acb3f9c08860c90eddbfc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 20:18:31 -0400 Subject: [PATCH] refactor(problems): give the graph toolkit its own module MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The list-based `Graph`, its encoding `encGraph`, the simple-graph reading `toSimpleGraph`, the executable adjacency `adjBool`, the subset verifier `verifySubset` and their certificates lived in `IndependentSet.lean`, and `Graph.lean` publicly imported `IndependentSet`. So every graph problem (Coloring, Hamiltonian, GraphIsomorphism, VertexCover) reached Karp's SAT-to-IS reduction and Cook–Levin through `Graph.lean`. The toolkit now lives in `Graph.lean`, which imports only the verifier layer, and `IndependentSet` imports `Graph`. `VertexCover`, which uses `IndependentSet`, imports it directly, and `GraphIsomorphism` imports Mathlib's `SimpleGraph.Maps` for `induce`. Adds `Graph.toSimpleGraph_adj`, the adjacency of the simple graph of an edge list, for clients that now unfold `toSimpleGraph` and `SimpleGraph.fromRel_adj`. It is deliberately not `simp`, since it would change the normal forms of existing proofs. Names, statements and proofs are otherwise unchanged. Refs #610 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Complexity/Problems/Graph.lean | 169 +++++++++++++++++- .../Complexity/Problems/GraphIsomorphism.lean | 1 + .../Complexity/Problems/IndependentSet.lean | 131 +------------- .../Complexity/Problems/VertexCover.lean | 2 +- 4 files changed, 166 insertions(+), 137 deletions(-) diff --git a/Complexity/Computability/Complexity/Problems/Graph.lean b/Complexity/Computability/Complexity/Problems/Graph.lean index d4fbbde9e3..51e493d09d 100644 --- a/Complexity/Computability/Complexity/Problems/Graph.lean +++ b/Complexity/Computability/Complexity/Problems/Graph.lean @@ -7,33 +7,56 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Complexity.Problems.IndependentSet +public import Complexity.Computability.Complexity.Classes.NP.Witness +public import Mathlib.Combinatorics.SimpleGraph.Basic import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat /-! -# Declared vertices of encoded graphs +# Graphs given by vertex and edge lists -Shared tools for the graph problems, whose graphs (`Cslib.Complexity.Graph`) are a list of -declared vertices, possibly with repetitions, and a list of edges. +The graph problems (`IndependentSet`, `Clique`, `VertexCover`, `KColoring`, the Hamiltonian +problems, `GraphIsomorphism`, …) take a graph (`Cslib.Complexity.Graph`) as a list of declared +vertices, possibly with repetitions, and a list of edges, encoded in binary +(`Cslib.Complexity.encGraph`). Its mathematical reading is a Mathlib simple graph on `ℕ` +(`Cslib.Complexity.Graph.toSimpleGraph`): two distinct vertices are adjacent when an edge joins +them in either direction. -* The distinct declared vertices (`Cslib.Complexity.Graph.distinctVertices`) are listed in - polynomial time by selecting every first occurrence (`Cslib.Complexity.selectDistinct`). -* Explicit verifiers with fixed certificate lengths write numbers in unary blocks of a certificate +This module holds the tools these problems share: + +* adjacency is tested in polynomial time (`Cslib.Complexity.Graph.adjBool`); +* a vertex subset problem with a pairwise condition, such as independent set or clique, is + verified by selecting distinct declared vertices with a certificate mask + (`Cslib.Complexity.Graph.verifySubset`, an instance of `Cslib.Complexity.subsetVerifier`); +* the distinct declared vertices (`Cslib.Complexity.Graph.distinctVertices`) are listed in + polynomial time by selecting every first occurrence (`Cslib.Complexity.selectDistinct`); +* explicit verifiers with fixed certificate lengths write numbers in unary blocks of a certificate (`Cslib.Complexity.unaryBlocks`): each number, at most `m`, gets its own block of `m` bits, and it is read back by counting the set bits of its block (`Cslib.Complexity.countP_unaryBlocks`). ## Main definitions +* `Cslib.Complexity.Graph`, `Cslib.Complexity.encGraph`, `Cslib.Complexity.Graph.toSimpleGraph`. +* `Cslib.Complexity.Graph.adjBool`: executable adjacency. +* `Cslib.Complexity.Graph.verifySubset`: the verifier of a vertex subset problem. * `Cslib.Complexity.Graph.distinctVertices`: the declared vertices without repetitions. * `Cslib.Complexity.unaryBlocks`: numbers written in unary blocks of a certificate. ## Main results +* `Cslib.Complexity.Graph.toSimpleGraph_adj`, `Cslib.Complexity.Graph.adjBool_eq_true_iff`: + adjacency. +* `Cslib.Complexity.Graph.isVerifier_verifySubset`, + `Cslib.Complexity.Graph.computableTidilyInPolyTime_verifySubset`: the subset verifier is a + polynomial-time verifier. * `Cslib.Complexity.Graph.length_vertices_le_encGraph`: a graph has no more declared vertices than the length of its encoding. * `Cslib.Complexity.countP_unaryBlocks`: counting the set bits of a block reads its number. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 2.4][AroraBarak09] -/ @[expose] public section @@ -42,6 +65,138 @@ namespace Cslib.Complexity open Turing.MultiTapeTM ComputableTidilyInPolyTime +/-- A graph on natural numbers, given by its vertices and its edges. -/ +abbrev Graph : Type := List ℕ × List (ℕ × ℕ) + +/-- Graphs encoded by framed lists of binary vertex labels and binary edge pairs. -/ +def encGraph : Graph ↪ List Bool := + encPair (encList encNat) (encList (encPair encNat encNat)) + +/-- The simple graph of an edge list: two distinct vertices are adjacent when an edge joins them, +in either direction. -/ +def Graph.toSimpleGraph (G : Graph) : SimpleGraph ℕ := SimpleGraph.fromRel fun u v => (u, v) ∈ G.2 + + +/-- Adjacency in the simple graph of an edge list: two distinct vertices joined by an edge in +either direction. It is not a `simp` lemma, so that the adjacency stays folded until a proof +unfolds it. -/ +theorem Graph.toSimpleGraph_adj {G : Graph} {u v : ℕ} : + G.toSimpleGraph.Adj u v ↔ u ≠ v ∧ ((u, v) ∈ G.2 ∨ (v, u) ∈ G.2) := + SimpleGraph.fromRel_adj _ _ _ + +namespace Graph + +/-! ### Subset verification on encoded graphs -/ + +/-- Executable adjacency test on an edge list: two distinct vertices are adjacent when an edge +joins them in either direction. -/ +def adjBool (G : Graph) (u v : ℕ) : Bool := + decide (u ≠ v) && + (G.2.any (fun e => decide (e = (u, v))) || G.2.any (fun e => decide (e = (v, u)))) + +@[simp] +theorem adjBool_eq_true_iff (G : Graph) (u v : ℕ) : + G.adjBool u v = true ↔ G.toSimpleGraph.Adj u v := by + simp [adjBool, toSimpleGraph, SimpleGraph.fromRel_adj] + +@[simp] +theorem adjBool_eq_false_iff (G : Graph) (u v : ℕ) : + G.adjBool u v = false ↔ ¬G.toSimpleGraph.Adj u v := by + rw [← Bool.not_eq_true, ← adjBool_eq_true_iff, Bool.not_eq_true] + +/-- Testing adjacency in an encoded graph is polynomial-time. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_adjBool : + ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => p.1.1.adjBool p.1.2 p.2) + (encPair (encPair encGraph encNat) encNat) encBool := by + unfold adjBool encGraph + fun_prop + +/-- Select distinct declared vertices from `V` using the certificate mask `w`: position `i` of `V` +is kept when bit `i` of `w` is `true` and `i` is the first occurrence of that vertex in `V`. This is +`Cslib.Complexity.selectDistinct` on vertex lists (`selectVertices_eq_selectDistinct`). -/ +def selectVertices (V : List ℕ) (w : List Bool) : List ℕ := + (V.zipIdx.filter fun p => w.getD p.2 false && decide (V.idxOf p.1 = p.2)).map Prod.fst + +theorem selectVertices_eq_selectDistinct : selectVertices = selectDistinct := rfl + +theorem mem_selectVertices {V : List ℕ} {w : List Bool} {v : ℕ} : + v ∈ selectVertices V w ↔ v ∈ V ∧ w.getD (V.idxOf v) false = true := + mem_selectDistinct + +theorem nodup_selectVertices (V : List ℕ) (w : List Bool) : (selectVertices V w).Nodup := + nodup_selectDistinct V w + +/-- Selecting distinct declared vertices from a certificate mask is polynomial-time. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_selectVertices : + ComputableTidilyInPolyTime (fun p : List ℕ × List Bool => selectVertices p.1 p.2) + (encPair (encList encNat) encBits) (encList encNat) := + computableTidilyInPolyTime_selectDistinct encNat + +/-- Verify a cardinality-`m` vertex subset problem with pairwise relation `rel`: select distinct +declared vertices from `G.1` by the certificate mask, compare the selected count with `m` in +binary, and test `rel` on all distinct selected pairs. -/ +def verifySubset (rel : Graph → ℕ → ℕ → Bool) : (Graph × ℕ) × List Bool → Bool := + subsetVerifier (fun x => x.1.1) fun y => + decide (y.2.length = y.1.2) && y.2.all fun u => y.2.all fun v => decide (u = v) || rel y.1.1 u v + +/-- A graph has no more declared vertices than the length of its encoded instance. -/ +theorem length_vertices_le (x : Graph × ℕ) : + x.1.1.length ≤ (encPair encGraph encNat x).length := by + calc x.1.1.length + ≤ (encList encNat x.1.1).length := length_le_length_encList encNat x.1.1 + _ ≤ (encGraph x.1).length := by + simp only [encGraph, length_encPair] + omega + _ ≤ (encPair encGraph encNat x).length := by + simp only [length_encPair] + omega + +/-- `verifySubset` is a polynomial-length verifier for any graph subset problem whose pairwise +relation agrees with `rel` on distinct vertices. -/ +theorem isVerifier_verifySubset {rel : Graph → ℕ → ℕ → Bool} {P : Graph → ℕ → ℕ → Prop} + (hrel : ∀ G u v, u ≠ v → (rel G u v = true ↔ P G u v)) : + IsVerifier (encPair encGraph encNat) Polynomial.X (verifySubset rel) + {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ (S : Set ℕ).Pairwise (P x.1) ∧ S.card = x.2} := by + refine isVerifier_subsetVerifier (fun x => by simpa using length_vertices_le x) + fun x l hl _ => ?_ + simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, Bool.or_eq_true, + List.toFinset_card_of_nodup hl, List.coe_toFinset] + refine ⟨fun ⟨hlen, h⟩ => ⟨fun u hu v hv huv => ?_, hlen⟩, + fun ⟨h, hlen⟩ => ⟨hlen, fun u hu v hv => ?_⟩⟩ + · exact (hrel x.1 u v huv).1 ((h u hu v hv).resolve_left huv) + · by_cases huv : u = v + · exact Or.inl huv + · exact Or.inr ((hrel x.1 u v huv).2 (h hu hv huv)) + +@[fun_prop] +private theorem bool_or' {α : Type} {encA : α ↪ List Bool} {left right : α → Bool} + (hleft : ComputableTidilyInPolyTime left encA encBool) + (hright : ComputableTidilyInPolyTime right encA encBool) : + ComputableTidilyInPolyTime (fun a => left a || right a) encA encBool := + bool_or.comp (hleft.prod hright) + +/-- `verifySubset` is computable in polynomial time whenever the pairwise test `rel` is. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_verifySubset {rel : Graph → ℕ → ℕ → Bool} + (hrel : ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => rel p.1.1 p.1.2 p.2) + (encPair (encPair encGraph encNat) encNat) encBool) : + ComputableTidilyInPolyTime (verifySubset rel) + (encPair (encPair encGraph encNat) encBits) encBool := by + refine computableTidilyInPolyTime_subsetVerifier (encγ := encNat) + (by unfold encGraph; fun_prop) (bool_and' ?_ ?_) + · exact (unary_to_binary.comp ((length_list encNat).comp (snd _ _))).decide_eq' (by fun_prop) + · apply allWithInput (snd _ _) + apply allWithInput ((snd _ _).comp (fst _ _)) + have hproj : ComputableTidilyInPolyTime + (fun p : (((Graph × ℕ) × List ℕ) × ℕ) × ℕ => ((p.1.1.1.1, p.1.2), p.2)) + (encPair (encPair (encPair (encPair encGraph encNat) (encList encNat)) encNat) encNat) + (encPair (encPair encGraph encNat) encNat) := by fun_prop + exact bool_or' (by fun_prop) (hrel.comp hproj) + +end Graph + namespace Graph /-! ### Declared vertices -/ diff --git a/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean b/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean index faacc3c9d4..712b6b6a7d 100644 --- a/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean +++ b/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.Problems.Graph +public import Mathlib.Combinatorics.SimpleGraph.Maps import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat diff --git a/Complexity/Computability/Complexity/Problems/IndependentSet.lean b/Complexity/Computability/Complexity/Problems/IndependentSet.lean index e68f8e59db..b1c5bcffd0 100644 --- a/Complexity/Computability/Complexity/Problems/IndependentSet.lean +++ b/Complexity/Computability/Complexity/Problems/IndependentSet.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Complexity.Classes.NP.Witness +public import Complexity.Computability.Complexity.Problems.Graph public import Complexity.Computability.Complexity.Problems.SAT public import Complexity.Computability.Complexity.Reduction public import Mathlib.Combinatorics.SimpleGraph.Clique @@ -41,10 +41,7 @@ first-order interpretations. ## Main definitions -* `Cslib.Complexity.Graph.toSimpleGraph`, `Cslib.Complexity.encGraph`, - `Cslib.Complexity.IndependentSet`. -* `Cslib.Complexity.Graph.adjBool`, `Cslib.Complexity.Graph.selectVertices`, - `Cslib.Complexity.Graph.verifySubset`. +* `Cslib.Complexity.IndependentSet`. * `Cslib.Complexity.IndependentSet.verifier`. * `Cslib.Complexity.SAT.toIndependentSet`. * `Cslib.Complexity.Graph.indepNum`: the independence number. @@ -76,135 +73,11 @@ namespace Cslib.Complexity open Cslib.Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime -/-- A graph on natural numbers, given by its vertices and its edges. -/ -abbrev Graph : Type := List ℕ × List (ℕ × ℕ) - -/-- Graphs encoded by framed lists of binary vertex labels and binary edge pairs. -/ -def encGraph : Graph ↪ List Bool := - encPair (encList encNat) (encList (encPair encNat encNat)) - -/-- The simple graph of an edge list: two distinct vertices are adjacent when an edge joins them, -in either direction. -/ -def Graph.toSimpleGraph (G : Graph) : SimpleGraph ℕ := SimpleGraph.fromRel fun u v => (u, v) ∈ G.2 - /-- The graphs with an independent set of `m` of their vertices [Arora and Barak, Section 2.4][AroraBarak09]. -/ def IndependentSet : Set (Graph × ℕ) := {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ x.1.toSimpleGraph.IsNIndepSet x.2 S} -namespace Graph - -/-! ### Subset verification on encoded graphs -/ - -/-- Executable adjacency test on an edge list: two distinct vertices are adjacent when an edge -joins them in either direction. -/ -def adjBool (G : Graph) (u v : ℕ) : Bool := - decide (u ≠ v) && - (G.2.any (fun e => decide (e = (u, v))) || G.2.any (fun e => decide (e = (v, u)))) - -@[simp] -theorem adjBool_eq_true_iff (G : Graph) (u v : ℕ) : - G.adjBool u v = true ↔ G.toSimpleGraph.Adj u v := by - simp [adjBool, toSimpleGraph, SimpleGraph.fromRel_adj] - -@[simp] -theorem adjBool_eq_false_iff (G : Graph) (u v : ℕ) : - G.adjBool u v = false ↔ ¬G.toSimpleGraph.Adj u v := by - rw [← Bool.not_eq_true, ← adjBool_eq_true_iff, Bool.not_eq_true] - -/-- Testing adjacency in an encoded graph is polynomial-time. -/ -@[fun_prop] -theorem computableTidilyInPolyTime_adjBool : - ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => p.1.1.adjBool p.1.2 p.2) - (encPair (encPair encGraph encNat) encNat) encBool := by - unfold adjBool encGraph - fun_prop - -/-- Select distinct declared vertices from `V` using the certificate mask `w`: position `i` of `V` -is kept when bit `i` of `w` is `true` and `i` is the first occurrence of that vertex in `V`. This is -`Cslib.Complexity.selectDistinct` on vertex lists (`selectVertices_eq_selectDistinct`). -/ -def selectVertices (V : List ℕ) (w : List Bool) : List ℕ := - (V.zipIdx.filter fun p => w.getD p.2 false && decide (V.idxOf p.1 = p.2)).map Prod.fst - -theorem selectVertices_eq_selectDistinct : selectVertices = selectDistinct := rfl - -theorem mem_selectVertices {V : List ℕ} {w : List Bool} {v : ℕ} : - v ∈ selectVertices V w ↔ v ∈ V ∧ w.getD (V.idxOf v) false = true := - mem_selectDistinct - -theorem nodup_selectVertices (V : List ℕ) (w : List Bool) : (selectVertices V w).Nodup := - nodup_selectDistinct V w - -/-- Selecting distinct declared vertices from a certificate mask is polynomial-time. -/ -@[fun_prop] -theorem computableTidilyInPolyTime_selectVertices : - ComputableTidilyInPolyTime (fun p : List ℕ × List Bool => selectVertices p.1 p.2) - (encPair (encList encNat) encBits) (encList encNat) := - computableTidilyInPolyTime_selectDistinct encNat - -/-- Verify a cardinality-`m` vertex subset problem with pairwise relation `rel`: select distinct -declared vertices from `G.1` by the certificate mask, compare the selected count with `m` in -binary, and test `rel` on all distinct selected pairs. -/ -def verifySubset (rel : Graph → ℕ → ℕ → Bool) : (Graph × ℕ) × List Bool → Bool := - subsetVerifier (fun x => x.1.1) fun y => - decide (y.2.length = y.1.2) && y.2.all fun u => y.2.all fun v => decide (u = v) || rel y.1.1 u v - -/-- A graph has no more declared vertices than the length of its encoded instance. -/ -theorem length_vertices_le (x : Graph × ℕ) : - x.1.1.length ≤ (encPair encGraph encNat x).length := by - calc x.1.1.length - ≤ (encList encNat x.1.1).length := length_le_length_encList encNat x.1.1 - _ ≤ (encGraph x.1).length := by - simp only [encGraph, length_encPair] - omega - _ ≤ (encPair encGraph encNat x).length := by - simp only [length_encPair] - omega - -/-- `verifySubset` is a polynomial-length verifier for any graph subset problem whose pairwise -relation agrees with `rel` on distinct vertices. -/ -theorem isVerifier_verifySubset {rel : Graph → ℕ → ℕ → Bool} {P : Graph → ℕ → ℕ → Prop} - (hrel : ∀ G u v, u ≠ v → (rel G u v = true ↔ P G u v)) : - IsVerifier (encPair encGraph encNat) Polynomial.X (verifySubset rel) - {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ (S : Set ℕ).Pairwise (P x.1) ∧ S.card = x.2} := by - refine isVerifier_subsetVerifier (fun x => by simpa using length_vertices_le x) - fun x l hl _ => ?_ - simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, Bool.or_eq_true, - List.toFinset_card_of_nodup hl, List.coe_toFinset] - refine ⟨fun ⟨hlen, h⟩ => ⟨fun u hu v hv huv => ?_, hlen⟩, - fun ⟨h, hlen⟩ => ⟨hlen, fun u hu v hv => ?_⟩⟩ - · exact (hrel x.1 u v huv).1 ((h u hu v hv).resolve_left huv) - · by_cases huv : u = v - · exact Or.inl huv - · exact Or.inr ((hrel x.1 u v huv).2 (h hu hv huv)) - -@[fun_prop] -private theorem bool_or' {α : Type} {encA : α ↪ List Bool} {left right : α → Bool} - (hleft : ComputableTidilyInPolyTime left encA encBool) - (hright : ComputableTidilyInPolyTime right encA encBool) : - ComputableTidilyInPolyTime (fun a => left a || right a) encA encBool := - bool_or.comp (hleft.prod hright) - -/-- `verifySubset` is computable in polynomial time whenever the pairwise test `rel` is. -/ -@[fun_prop] -theorem computableTidilyInPolyTime_verifySubset {rel : Graph → ℕ → ℕ → Bool} - (hrel : ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => rel p.1.1 p.1.2 p.2) - (encPair (encPair encGraph encNat) encNat) encBool) : - ComputableTidilyInPolyTime (verifySubset rel) - (encPair (encPair encGraph encNat) encBits) encBool := by - refine computableTidilyInPolyTime_subsetVerifier (encγ := encNat) - (by unfold encGraph; fun_prop) (bool_and' ?_ ?_) - · exact (unary_to_binary.comp ((length_list encNat).comp (snd _ _))).decide_eq' (by fun_prop) - · apply allWithInput (snd _ _) - apply allWithInput ((snd _ _).comp (fst _ _)) - have hproj : ComputableTidilyInPolyTime - (fun p : (((Graph × ℕ) × List ℕ) × ℕ) × ℕ => ((p.1.1.1.1, p.1.2), p.2)) - (encPair (encPair (encPair (encPair encGraph encNat) (encList encNat)) encNat) encNat) - (encPair (encPair encGraph encNat) encNat) := by fun_prop - exact bool_or' (by fun_prop) (hrel.comp hproj) - -end Graph - namespace SAT /-! ### Karp's reduction -/ diff --git a/Complexity/Computability/Complexity/Problems/VertexCover.lean b/Complexity/Computability/Complexity/Problems/VertexCover.lean index f9a5691873..9814158514 100644 --- a/Complexity/Computability/Complexity/Problems/VertexCover.lean +++ b/Complexity/Computability/Complexity/Problems/VertexCover.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Complexity.Problems.Graph +public import Complexity.Computability.Complexity.Problems.IndependentSet public import Mathlib.Combinatorics.SimpleGraph.VertexCover import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List