Graphs given by vertex and edge lists

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), or the simple graph induced on the subtype of declared vertices (Cslib.Complexity.Graph.induced): two distinct vertices are adjacent when an edge joins them in either direction.

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), and their positions enumerate the declared vertices (Cslib.Complexity.Graph.vertexEquiv);
• 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);
• a vertex ordering problem, such as Hamiltonian path/cycle, TSP or graph isomorphism, is verified by decoding a list of vertices from unary blocks of a certificate (Cslib.Complexity.Graph.decodeVertexList) and checking that it lists every vertex of the target list without repetitions (Cslib.Complexity.Graph.enumeratesBool, Cslib.Complexity.Graph.verifyOrdering).

Main definitions

• Cslib.Complexity.Graph, Cslib.Complexity.encGraph, Cslib.Complexity.Graph.toSimpleGraph, Cslib.Complexity.Graph.induced.
• Cslib.Complexity.Graph.adjBool: executable adjacency.
• Cslib.Complexity.Graph.verifySubset: the verifier of a vertex subset problem.
• Cslib.Complexity.Graph.distinctVertices, Cslib.Complexity.Graph.vertexEquiv: the declared vertices without repetitions and their enumeration by positions.
• Cslib.Complexity.unaryBlocks: numbers written in unary blocks of a certificate.
• Cslib.Complexity.Graph.enumeratesBool, Cslib.Complexity.Graph.decodeVertexList, Cslib.Complexity.Graph.verifyOrdering: verifying orderings of a vertex list.

Main results

• Cslib.Complexity.Graph.toSimpleGraph_adj, Cslib.Complexity.Graph.induced_adj, Cslib.Complexity.Graph.adjBool_eq_true_iff: adjacency.
• Cslib.Complexity.Graph.computableInPolyTime_adjBool, Cslib.Complexity.Graph.computableInPolyTime_adjBool_comp: testing adjacency is polynomial-time.
• Cslib.Complexity.Graph.isVerifier_verifySubset, Cslib.Complexity.Graph.computableInPolyTime_verifySubset: the subset verifier is a polynomial-time verifier.
• Cslib.Complexity.Graph.length_vertices_le_encGraph, Cslib.Complexity.Graph.length_vertices_add_length_edges_le_encGraph: a graph lists no more vertices, or vertices and edges, than the length of its encoding.
• Cslib.Complexity.countP_unaryBlocks: counting the set bits of a block reads its number.
• Cslib.Complexity.Graph.exists_decodeVertexList_eq, Cslib.Complexity.Graph.isVerifier_verifyOrdering, Cslib.Complexity.Graph.computableInPolyTime_verifyOrdering: the ordering verifier is a polynomial-time verifier with quadratic certificate length.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.4

structure Cslib.Complexity.Graph : Type

A graph on natural numbers, given by its vertices and its edges.

• vertices : List ℕ

  The declared vertices of the graph, possibly with repetitions.

• edges : List (ℕ × ℕ)

  The declared edges of the graph as pairs of vertex identifiers.

theorem Cslib.Complexity.Graph.ext {x y : Graph} (vertices : x.vertices = y.vertices) (edges : x.edges = y.edges) : x = y

theorem Cslib.Complexity.Graph.ext_iff {x y : Graph} : x = y ↔ x.vertices = y.vertices ∧ x.edges = y.edges

def Cslib.Complexity.instDecidableEqGraph.decEq (x✝ x✝¹ : Graph) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqGraph : DecidableEq Graph

def Cslib.Complexity.instReprGraph.repr : Graph → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprGraph : Repr Graph

@[instance_reducible]

instance Cslib.Complexity.instInhabitedGraph : Inhabited Graph

theorem Cslib.Complexity.encGraph_edges_inO : Turing.MultiTapeTM.ComputableInO Graph.edges encGraph (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (fun (a : Graph) => (encGraph a).length) fun (a : Graph) => (encGraph a).length

theorem Cslib.Complexity.encGraph_vertices_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Graph} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encGraph S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).vertices) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.encGraph_vertices_deg : Turing.MultiTapeTM.ComputableInDegree Graph.vertices encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

@[reducible, inline]

abbrev Cslib.Complexity.encGraphFields : List ℕ × List (ℕ × ℕ) ↪ List Bool

The tuple of the fields of encGraph.

theorem Cslib.Complexity.encGraph_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {T0 S0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { vertices := x0 x, edges := x1 x }) encIn encGraph (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encGraph_edges_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Graph} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encGraph S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).edges) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) S✝

theorem Cslib.Complexity.encGraph_vertices_inO : Turing.MultiTapeTM.ComputableInO Graph.vertices encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : Graph) => (encGraph a).length) fun (a : Graph) => (encGraph a).length

theorem Cslib.Complexity.encGraph_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List ℕ} {x1 : γ → List (ℕ × ℕ)} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { vertices := x0 x, edges := x1 x }) encIn encGraph budget

theorem Cslib.Complexity.encGraph_vertices_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Graph} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encGraph → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).vertices) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.encGraph_edges_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Graph} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encGraph → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).edges) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

theorem Cslib.Complexity.encGraph_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List ℕ × List (ℕ × ℕ)) => { vertices := p.1, edges := p.2 }) encGraphFields encGraph 1 1

theorem Cslib.Complexity.encGraph_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {x1 : γ → List (ℕ × ℕ)} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { vertices := x0 x, edges := x1 x }) encIn encGraph

@[simp]

theorem Cslib.Complexity.encGraph_apply (a : Graph) : encGraph a = encGraphFields (a.vertices, a.edges)

theorem Cslib.Complexity.encGraph_edges_deg : Turing.MultiTapeTM.ComputableInDegree Graph.edges encGraph (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) 1 1

def Cslib.Complexity.encGraph : Graph ↪ List Bool

Graphs encoded by framed lists of binary vertex labels and binary edge pairs.

theorem Cslib.Complexity.encGraph_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Graph) => (a.vertices, a.edges)) encGraph encGraphFields 1 1

def Cslib.Complexity.Graph.toSimpleGraph (G : Graph) : SimpleGraph ℕ

The simple graph of an edge list: two distinct vertices are adjacent when an edge joins them, in either direction.

theorem Cslib.Complexity.Graph.toSimpleGraph_adj {G : Graph} {u v : ℕ} : G.toSimpleGraph.Adj u v ↔ u ≠ v ∧ ((u, v) ∈ G.edges ∨ (v, u) ∈ G.edges)

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.

def Cslib.Complexity.Graph.induced (G : Graph) : SimpleGraph { v : ℕ // v ∈ G.vertices }

The simple graph induced by G on its declared vertices.

@[simp]

theorem Cslib.Complexity.Graph.induced_adj {G : Graph} {u v : { v : ℕ // v ∈ G.vertices }} : G.induced.Adj u v ↔ G.toSimpleGraph.Adj ↑u ↑v

Declared vertices

theorem Cslib.Complexity.Graph.length_vertices_le_encGraph (G : Graph) : G.vertices.length ≤ (encGraph G).length

A graph has no more declared vertices than the length of its encoding.

theorem Cslib.Complexity.Graph.length_vertices_add_length_edges_le_encGraph (G : Graph) : G.vertices.length + G.edges.length ≤ (encGraph G).length

A graph lists no more vertices and edges than the length of its encoding.

def Cslib.Complexity.Graph.distinctVertices (G : Graph) : List ℕ

The declared vertices of G without repetitions, in the order of their first occurrences.

theorem Cslib.Complexity.Graph.mem_distinctVertices {G : Graph} {v : ℕ} : v ∈ G.distinctVertices ↔ v ∈ G.vertices

The distinct declared vertices are the declared vertices.

theorem Cslib.Complexity.Graph.nodup_distinctVertices (G : Graph) : G.distinctVertices.Nodup

The distinct declared vertices are listed without repetitions.

theorem Cslib.Complexity.Graph.length_distinctVertices (G : Graph) : G.distinctVertices.length = G.vertices.toFinset.card

The distinct declared vertices are as many as the elements of the vertex list.

theorem Cslib.Complexity.Graph.length_distinctVertices_le (G : Graph) : G.distinctVertices.length ≤ (encGraph G).length

A graph has no more distinct vertices than the length of its encoding.

def Cslib.Complexity.Graph.vertexEquiv (G : Graph) : Fin G.distinctVertices.length ≃ { v : ℕ // v ∈ G.vertices }

Positions in G.distinctVertices enumerate the declared vertices.

theorem Cslib.Complexity.Graph.vertexEquiv_apply (G : Graph) (i : Fin G.distinctVertices.length) : ↑(G.vertexEquiv i) = G.distinctVertices.getD (↑i) 0

@[simp]

theorem Cslib.Complexity.Graph.card_vertexSubtype (G : Graph) : Fintype.card { v : ℕ // v ∈ G.vertices } = G.vertices.toFinset.card

theorem Cslib.Complexity.Graph.natCard_vertexSubtype (G : Graph) : Nat.card { v : ℕ // v ∈ G.vertices } = G.vertices.toFinset.card

theorem Cslib.Complexity.Graph.computableInPolyTime_distinctVertices : Turing.MultiTapeTM.ComputableInPolyTime distinctVertices encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Listing the distinct vertices is polynomial-time.

Subset verification on encoded graphs

def Cslib.Complexity.Graph.adjBool (G : Graph) (u v : ℕ) : Bool

Executable adjacency test on an edge list: two distinct vertices are adjacent when an edge joins them in either direction.

@[simp]

theorem Cslib.Complexity.Graph.adjBool_eq_true_iff (G : Graph) (u v : ℕ) : G.adjBool u v = true ↔ G.toSimpleGraph.Adj u v

@[simp]

theorem Cslib.Complexity.Graph.adjBool_eq_false_iff (G : Graph) (u v : ℕ) : G.adjBool u v = false ↔ ¬G.toSimpleGraph.Adj u v

theorem Cslib.Complexity.Graph.computableInPolyTime_adjBool : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × ℕ) × ℕ) => p.1.1.adjBool p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Testing adjacency in an encoded graph is polynomial-time.

theorem Cslib.Complexity.Graph.computableInPolyTime_adjBool_comp {γ : Type} {enc : γ ↪ List Bool} {G : γ → Graph} {u v : γ → ℕ} (hG : Turing.MultiTapeTM.ComputableInPolyTime G enc encGraph) (hu : Turing.MultiTapeTM.ComputableInPolyTime u enc Turing.MultiTapeTM.encNat) (hv : Turing.MultiTapeTM.ComputableInPolyTime v enc Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : γ) => (G c).adjBool (u c) (v c)) enc Turing.MultiTapeTM.encBool

Testing adjacency between computed vertices of a computed graph is polynomial-time. This is Cslib.Complexity.Graph.computableInPolyTime_adjBool in the compositional form that fun_prop uses.

def Cslib.Complexity.Graph.verifySubset (rel : Graph → ℕ → ℕ → Bool) : (Graph × ℕ) × List Bool → Bool

Verify a cardinality-m vertex subset problem with pairwise relation rel: select distinct declared vertices from G.vertices by the certificate mask, compare the selected count with m in binary, and test rel on all distinct selected pairs.

theorem Cslib.Complexity.Graph.exists_subtype_pairwise_iff {G : Graph} {P : ℕ → ℕ → Prop} {m : ℕ} : (∃ (S : Finset { v : ℕ // v ∈ G.vertices }), ((↑S).Pairwise fun (u v : { v : ℕ // v ∈ G.vertices }) => P ↑u ↑v) ∧ S.card = m) ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ (↑S).Pairwise P ∧ S.card = m

A finite subset of declared vertices with a pairwise property corresponds to a finite subset of ℕ contained in G.vertices with the same pairwise property and cardinality.

theorem Cslib.Complexity.Graph.isVerifier_verifySubset {rel : Graph → ℕ → ℕ → Bool} {P : Graph → ℕ → ℕ → Prop} (hrel : ∀ (G : Graph) (u v : ℕ), u ≠ v → (rel G u v = true ↔ P G u v)) : IsVerifier (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) Polynomial.X (verifySubset rel) {x : Graph × ℕ | ∃ (S : Finset { v : ℕ // v ∈ x.1.vertices }), ((↑S).Pairwise fun (u v : { v : ℕ // v ∈ x.1.vertices }) => P x.1 ↑u ↑v) ∧ S.card = x.2}

verifySubset is a polynomial-length verifier for any graph subset problem whose pairwise relation agrees with rel on distinct vertices.

theorem Cslib.Complexity.Graph.computableInPolyTime_verifySubset {rel : Graph → ℕ → ℕ → Bool} (hrel : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × ℕ) × ℕ) => rel p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (verifySubset rel) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

verifySubset is computable in polynomial time whenever the pairwise test rel is.

Unary blocks

def Cslib.Complexity.unaryBlocks (m N : ℕ) (f : ℕ → ℕ) : List Bool

The certificate of N bits writing the numbers f a in unary blocks of width m: bit m * a + c is set when c < f a.

@[simp]

theorem Cslib.Complexity.length_unaryBlocks (m N : ℕ) (f : ℕ → ℕ) : (unaryBlocks m N f).length = N

theorem Cslib.Complexity.countP_unaryBlocks {m N a : ℕ} {f : ℕ → ℕ} (hf : f a ≤ m) (hN : m * (a + 1) ≤ N) : List.countP (fun (c : ℕ) => (unaryBlocks m N f).getD (m * a + c) false) (List.range m) = f a

Counting the set bits of block a of unaryBlocks m N f reads f a, when f a fits in the block and the block fits in the certificate.

Ordering verification

def Cslib.Complexity.Graph.enumeratesBool (V p : List ℕ) : Bool

Executable test that p lists every vertex of V exactly once and nothing else.

theorem Cslib.Complexity.Graph.enumeratesBool_eq_true_iff {V p : List ℕ} : enumeratesBool V p = true ↔ p.Nodup ∧ ∀ (v : ℕ), v ∈ p ↔ v ∈ V

enumeratesBool V p holds exactly when p lists the members of V without repetition.

def Cslib.Complexity.Graph.decodeVertexList (V : List ℕ) (w : List Bool) : List ℕ

The list of vertices described by a certificate w, for a vertex list V of length m: w is read as blocks of m bits, one for each distinct vertex of V, and the block numbered a names the entry of V whose position is its number of set bits, or 0 if there is none.

theorem Cslib.Complexity.Graph.exists_decodeVertexList_eq {V p : List ℕ} (hp : p.Nodup) (hpV : ∀ (v : ℕ), v ∈ p ↔ v ∈ V) {n : ℕ} (hn : V.length ≤ n) : ∃ (w : List Bool), w.length = n ^ 2 ∧ decodeVertexList V w = p

Every list of the distinct vertices of V, each listed once, is described by a certificate of length n ^ 2, for every n at least the length of V.

def Cslib.Complexity.Graph.verifyOrdering {α : Type} (V : α → List ℕ) (check : α → List ℕ → Bool) (x : α × List Bool) : Bool

Verify a vertex ordering problem: decode a list of vertices from the certificate (decodeVertexList), check that it lists every vertex of V x exactly once, and test it with check.

theorem Cslib.Complexity.Graph.isVerifier_verifyOrdering {α : Type} {enc : α ↪ List Bool} {V : α → List ℕ} {check : α → List ℕ → Bool} {P : α → List ℕ → Prop} (hV : ∀ (a : α), (V a).length ≤ (enc a).length) (hcheck : ∀ (a : α) (p : List ℕ), check a p = true ↔ P a p) : IsVerifier enc (Polynomial.X ^ 2) (verifyOrdering V check) {a : α | ∃ (p : List ℕ), p.Nodup ∧ (∀ (v : ℕ), v ∈ p ↔ v ∈ V a) ∧ P a p}

verifyOrdering verifies the existence of an ordering of the vertices satisfying P, with certificates of length n ^ 2 for instances of encoded length n, as long as check decides P and the vertex list is not longer than the encoded instance.

theorem Cslib.Complexity.Graph.computableInPolyTime_enumeratesBool : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : List ℕ × List ℕ) => enumeratesBool x.1 x.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool

Testing whether a list lists every vertex of another exactly once is polynomial-time.

theorem Cslib.Complexity.Graph.computableInPolyTime_decodeVertexList : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : List ℕ × List Bool) => decodeVertexList x.1 x.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Decoding a list of vertices from a certificate is polynomial-time.

theorem Cslib.Complexity.Graph.computableInPolyTime_verifyOrdering {α : Type} {enc : α ↪ List Bool} {V : α → List ℕ} {check : α → List ℕ → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hcheck : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : α × List ℕ) => check q.1 q.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (verifyOrdering V check) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

verifyOrdering is polynomial-time whenever the vertex list and the test check are.