The row arcs of a diamond to Label after a HAMPATH copy site

DefinitionThe row arcs of a diamond#✓fully proved

For natural numbers \(m\) (the number of clauses), \(i\) and \(l\), let \(r_{i,l} = m + i(3m + 2) + 1 + l\) be row vertex \(l\) of diamond \(i\). The row arcs between row vertices \(l\) and \(l + 1\) of diamond \(i\) are the list of the two arcs \((r_{i,l}, r_{i,l+1})\) and \((r_{i,l+1}, r_{i,l})\).

def rowE (m i l : ℕ) : List (ℕ × ℕ) := [(hpR m i l, hpR m i (l + 1)), (hpR m i (l + 1), hpR m i l)]

Uses 1 · Used by 4

Statement usesRow vertices of a diamond

Used byThe row loop of a diamond in the HAMPATH emitter · One diamond · The row of a diamond in the HAMPATH emitter · Correctness and running time of the HAMPATH emitter

DefinitionClause detours in a diamond#✓fully proved

For natural numbers \(m\) (the number of clauses), \(i\), \(x\) and \(j\), let \(r_{i,l} = m + i(3m + 2) + 1 + l\) be row vertex \(l\) of diamond \(i\). For a clause \(C\), a list of literals, the detours of clause \(j\) with contents \(C\) in diamond \(i\) of variable \(x\) are the list of the arcs \((r_{i,3j+1}, j)\) and \((j, r_{i,3j+2})\) if the positive literal \(x\) is in \(C\), followed by the arcs \((r_{i,3j+2}, j)\) and \((j, r_{i,3j+1})\) if the negative literal \(\lnot x\) is in \(C\).

def detE (m i x j : ℕ) (C : CNFClause) : List (ℕ × ℕ) :=
  (if (x, true) ∈ C then [(hpR m i (3 * j + 1), j), (j, hpR m i (3 * j + 2))] else []) ++
    (if (x, false) ∈ C then [(hpR m i (3 * j + 2), j), (j, hpR m i (3 * j + 1))] else [])

Uses 2 · Used by 5

Statement usesRow vertices of a diamond · CNF clause

Used byOne clause of the detour walk · The detour walk of a diamond in the HAMPATH emitter · The detours of a diamond · One diamond · Correctness and running time of the HAMPATH emitter

TheoremThe next diamond top follows the row#✓fully proved

For natural numbers \(m\) (the number of clauses) and \(i\), write \(t_i = m + i(3m + 2)\) for the top of diamond \(i\) and \(r_{i,l} = t_i + 1 + l\) for its row vertex \(l\). Then \(t_{i+1} = r_{i,3m} + 1\): the top of diamond \(i + 1\) comes right after the last row vertex of diamond \(i\).

theorem hpT_succ_eq_hpR (m i : ℕ) : hpT m (i + 1) = hpR m i (3 * m) + 1

Uses 2 · Used by 3

Statement usesRow vertices of a diamond · Tops of the diamonds

Used byFront of a diamond · One diamond · Correctness and running time of the HAMPATH emitter

TheoremSplitting off the middle clause of a concatenation#✓fully proved

Let \(P\) and \(Q\) be CNF formulas, \(C\) a clause, and \(\varphi\) the formula whose clauses are those of \(P\), then \(C\), then those of \(Q\). Write \(|P|\) for the number of clauses of \(P\) and \(\varphi_j\) for clause \(j\) of \(\varphi\), counting from \(0\) (the empty clause if \(j\) is out of range). Let \(f\) map each natural number \(j\) and clause to a list of elements of a type \(\alpha\). Then concatenating the lists \(f(j, \varphi_j)\) over \(j < |P| + 1\) in increasing order gives the concatenation of the lists \(f(j, \varphi_j)\) over \(j < |P|\), followed by \(f(|P|, C)\).

theorem range_flatMap_getD {α : Type} (f : ℕ → CNFClause → List α) (pre : CNF) (C : CNFClause)
    (post : CNF) :
    (List.range (pre.length + 1)).flatMap (fun j => f j ((pre ++ C :: post).getD j [])) =
      (List.range pre.length).flatMap (fun j => f j ((pre ++ C :: post).getD j [])) ++
        f pre.length C

Uses 2 · Used by 1

Statement usesCNF formula · CNF clause

Used byThe detour walk of a diamond in the HAMPATH emitter

DefinitionInsert a variable if new#✓fully proved

For a natural number \(x\) and a list \(V\) of natural numbers, inserting \(x\) into \(V\) gives \(V\) itself if \(x\) occurs in \(V\), and otherwise the list obtained by prepending \(x\) to \(V\).

def insV (x : ℕ) (vs : List ℕ) : List ℕ := if x ∈ vs then vs else x :: vs

Used by 6

Used byRemoving duplicates by insertion · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · Phase A of the HAMPATH emitter

TheoremRemoving duplicates by insertion#✓fully proved

For every list \(l\) of natural numbers, folding \(l\) from the right into the empty list, prepending each element unless it is already present, gives \(l\) with duplicates removed: each element is kept at its last occurrence in \(l\), in order.

theorem foldr_insV (l : List ℕ) : l.foldr insV [] = l.dedup

Uses 1 · Used by 1

Statement usesInsert a variable if new

Used byPhase A of the HAMPATH emitter

TheoremConsecutive row vertices#✓fully proved

In the HAMPATH construction with \(m\) clauses, for every diamond \(i\) and every \(l \in \mathbb{N}\), row vertex \(l + 1\) of diamond \(i\) is one more than row vertex \(l\) of diamond \(i\).

theorem hpR_succ (m i l : ℕ) : hpR m i (l + 1) = hpR m i l + 1

Uses 2 · Used by 3

Statement usesRow vertices of a diamond

Proof usesTops of the diamonds

Used byOne clause of the detour walk · The row loop of a diamond in the HAMPATH emitter · One diamond

TheoremLength bound for the bit encoding of an edge list#✓fully proved

Let \(B\) be a natural number and \(E\) a list of pairs of natural numbers such that every pair \((u, v)\) in \(E\) has \(u \le B\) and \(v \le B\). Then the bit encoding of \(E\), which writes each pair \((u, v)\) as \(u\) ones, a zero, \(v\) ones and a zero, has length at most \(|E| \cdot (2B + 2)\), where \(|E|\) is the length of \(E\).

theorem edgeBits_length_le (B : ℕ) : ∀ (es : List (ℕ × ℕ)), (∀ e ∈ es, e.1 ≤ B ∧ e.2 ≤ B) →
    (Karp.edgeBits es).length ≤ es.length * (2 * B + 2)

Uses 2 · Used by 1

Statement usesBit encoding of an edge list

Proof usesBits of an edge list, first edge first

Used byCorrectness and running time of the HAMPATH emitter

InductiveStacks of the HAMPATH emitter#✓fully proved

The emitter has eighteen distinct stacks: \(T\) (the tokens), \(O\) (the output), \(F\) (the tokens in reading order), \(V\) (the distinct variables), \(W\) (the other side of the walk over \(V\)), \(Q\) (the edges in progress), \(G\) (garbage), \(X\) and \(Y\) (comparison scratch), \(C\) (the clause count), \(M\) (three times the clause count), \(P\) (the diamond top), \(N\) (the row end), \(R\) (the row vertex), \(L\) (the row loop index), \(J\) (the clause index), \(D\) (the detour vertex) and \(Z\) (copy scratch).

inductive K | T | O | F | V | W | Q | G | X | Y | C | M | P | N | R | L | J | D | Z
  deriving DecidableEq

Used by 34

Used byStack of a HAMPATH copy-site counter · Stack alphabets of the HAMPATH emitter · HAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Running a chain of copy sites in the HAMPATH emitter · Comparing a name with the top entry of the variable stack · Copying a counter in the HAMPATH emitter · The HAMPATH emitter machine · Run of a HAMPATH copy site · Stacks of a quiescent emitter state · HAMPATH emitter, phase A: one clause · Adding units along no stacks · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · Draining a counter · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time

DefinitionStack alphabets of the HAMPATH emitter#✓fully proved

The alphabet of the output stack \(O\) is the set of bits (booleans); every other stack has the token symbols as its alphabet.

The counter stacks only ever hold the symbol \(\mathrm{cl}\).

@[reducible] def Γ : K → Type
  | .O => Bool
  | _ => Sym

Uses 2 · Used by 33

Statement usesStacks of the HAMPATH emitter · Stack alphabet of the SAT verifier

Used byUnit symbol of an emitter counter · HAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Running a chain of copy sites in the HAMPATH emitter · Comparing a name with the top entry of the variable stack · Copying a counter in the HAMPATH emitter · The HAMPATH emitter machine · Run of a HAMPATH copy site · Stacks of a quiescent emitter state · HAMPATH emitter, phase A: one clause · Adding units along no stacks · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · Draining a counter · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time

InductiveCounters read by HAMPATH copy sites#✓fully proved

The type with the five elements \(p, n, r, j, d\), naming the counters of the HAMPATH emitter that a copy site can read: the diamond top \(p\), the row end \(n\), the row vertex \(r\), the clause index \(j\) and the detour vertex \(d\).

inductive Src | p | n | r | j | d
  deriving DecidableEq

Used by 10

Used byStack of a HAMPATH copy-site counter · Counter read by a copy site · Unit symbol of an emitter counter · Running a chain of copy sites in the HAMPATH emitter · Run of a HAMPATH copy site · Counter values of a quiescent emitter state · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter

DefinitionStack of a HAMPATH copy-site counter#✓fully proved

The counters \(p\), \(n\), \(r\), \(j\), \(d\) that a copy site of the HAMPATH emitter reads are held on the emitter's stacks \(P\), \(N\), \(R\), \(J\), \(D\) respectively (the diamond top, the row end, the row vertex, the clause index and the detour vertex).

def Src.k : Src → K
  | .p => .P
  | .n => .N
  | .r => .R
  | .j => .J
  | .d => .D

Uses 2 · Used by 3

Statement usesStacks of the HAMPATH emitter · Counters read by HAMPATH copy sites

Used byUnit symbol of an emitter counter · The HAMPATH emitter machine · Run of a HAMPATH copy site

DefinitionUnit symbol of an emitter counter#✓fully proved

For every counter \(s\) read by copy sites, the unit symbol of \(s\) is the token symbol \(\mathrm{cl}\), as a letter of the alphabet of the stack that holds \(s\).

def Src.unit : (s : Src) → Γ s.k
  | .p => Sym.cl
  | .n => Sym.cl
  | .r => Sym.cl
  | .j => Sym.cl
  | .d => Sym.cl

Uses 4 · Used by 2

Statement usesCounters read by HAMPATH copy sites · Stack of a HAMPATH copy-site counter · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier

Used byThe HAMPATH emitter machine · Run of a HAMPATH copy site

InductiveCopy sites of the HAMPATH emitter#✓fully proved

The type of the twenty copy sites of the emitter machine. Each site writes one endpoint of an edge of the emitted HAMPATH instance, \(u\) for the source and \(v\) for the target: the sites \(f_iu, f_iv\) for \(i = 1, \dots, 4\) belong to the four frame edges, \(w_iu, w_iv\) for \(i = 1, 2\) to the two row edges, and \(d_iu, d_iv\) for \(i = 1, \dots, 4\) to the detour edges, positive for \(i = 1, 2\) and negative for \(i = 3, 4\).

inductive Site
  | f1u | f1v | f2u | f2v | f3u | f3v | f4u | f4v | w1u | w1v | w2u | w2v
  | d1u | d1v | d2u | d2v | d3u | d3v | d4u | d4v
  deriving DecidableEq

Used by 19

Used byCopy sites of the HAMPATH emitter, listed · Extra ones of a copy site · Labels of the HAMPATH emitter · Label after a HAMPATH copy site · Counter read by a copy site · Bits pushed by a copy site of the HAMPATH emitter · Copy sites chained in the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · End of a clause in the detour walk · The HAMPATH emitter machine · Run of a HAMPATH copy site · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter · Frame copy sites of the HAMPATH emitter · Row copy sites of the HAMPATH emitter · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time

DefinitionCopy sites of the HAMPATH emitter, listed#✓fully proved

The list of the twenty copy sites of the HAMPATH emitter, in this order: the frame sites \(f_1u, f_1v, f_2u, f_2v, f_3u, f_3v, f_4u, f_4v\), the row sites \(w_1u, w_1v, w_2u, w_2v\), and the detour sites \(d_1u, d_1v, d_2u, d_2v, d_3u, d_3v, d_4u, d_4v\).

def Site.all : List Site :=
  [.f1u, .f1v, .f2u, .f2v, .f3u, .f3v, .f4u, .f4v, .w1u, .w1v, .w2u, .w2v,
    .d1u, .d1v, .d2u, .d2v, .d3u, .d3v, .d4u, .d4v]

Uses 1 · Used by 1

Statement usesCopy sites of the HAMPATH emitter

Used bySAT ≤ HAMPATH is polynomial-time

DefinitionCounter read by a copy site#✓fully proved

The map from copy sites to counters sending \(f_1u, f_1v, f_2u, f_3u\) to the diamond top \(p\); \(f_2v, f_3v, f_4u, f_4v\) to the row end \(n\); \(w_1u, w_1v, w_2u, w_2v\) to the row vertex \(r\); \(d_1u, d_2v, d_3u, d_4v\) to the detour vertex \(d\); and \(d_1v, d_2u, d_3v, d_4u\) to the clause index \(j\).

def Site.src : Site → Src
  | .f1u | .f1v | .f2u | .f3u => .p
  | .f2v | .f3v | .f4u | .f4v => .n
  | .w1u | .w1v | .w2u | .w2v => .r
  | .d1u | .d2v | .d3u | .d4v => .d
  | .d1v | .d2u | .d3v | .d4u => .j

Uses 2 · Used by 8

Statement usesCopy sites of the HAMPATH emitter · Counters read by HAMPATH copy sites

Used byBits pushed by a copy site of the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · The HAMPATH emitter machine · Run of a HAMPATH copy site · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter

DefinitionExtra ones of a copy site#✓fully proved

The number of extra ones a copy site adds to its counter's value is \(1\) for the sites \(f_{1v}\), \(f_{3u}\), \(f_{3v}\), \(f_{4v}\), \(w_{1v}\), \(w_{2u}\), \(d_{2v}\) and \(d_{3u}\), and \(0\) for every other site.

def Site.ext : Site → ℕ
  | .f1v | .f3u | .f3v | .f4v | .w1v | .w2u | .d2v | .d3u => 1
  | _ => 0

Uses 1 · Used by 7

Statement usesCopy sites of the HAMPATH emitter

Used byBits pushed by a copy site of the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · The HAMPATH emitter machine · Run of a HAMPATH copy site · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter

InductiveLabels of the HAMPATH emitter#✓fully proved

Let \(f\), \(p_p\), \(p_n\) and \(b\) range over bits and \(j\) over copy sites. A label of the emitter is one of \(\mathrm{a0}\), \(\mathrm{anm}\), \(\mathrm{aw}(f)\), \(\mathrm{ac}(f)\), \(\mathrm{ar1}(f)\), \(\mathrm{ar2}(f)\), \(\mathrm{amv}(f)\), \(\mathrm{asep}(f)\), \(\mathrm{ab}(f)\), \(\mathrm{ad2}\), \(\mathrm{ad3}\), \(\mathrm{b0}\), \(\mathrm{b1}\), \(\mathrm{h0}, \dots, \mathrm{h5}\), \(\mathrm{r0}, \dots, \mathrm{r4}\), \(\mathrm{wi}\), \(\mathrm{e0}\), \(\mathrm{e1}\), \(\mathrm{e2}\), \(\mathrm{dw}(p_p, p_n)\), \(\mathrm{dk}(p_p, p_n)\), \(\mathrm{dr1}(p_p, p_n, b)\), \(\mathrm{dr2}(p_p, p_n, b)\), \(\mathrm{dm}(p_p, p_n, b)\), \(\mathrm{dl}(p_p, p_n, b)\), \(\mathrm{dj}\), \(\mathrm{t0}, \dots, \mathrm{t8}\), \(\mathrm{z0}, \dots, \mathrm{z9}\), \(\mathrm{cpA}(j, b)\), \(\mathrm{cpB}(j, b)\), \(\mathrm{post}(j, b)\) and \(\mathrm{done}\), all distinct.

Their roles, in terms of the emitter's stacks: in phase A, \(\mathrm{a0}\) reads a token, \(\mathrm{anm}\) moves a name to \(F\), and \(\mathrm{aw}(f)\) to \(\mathrm{asep}(f)\) walk \(V\), with \(f\) recording whether a match was found (\(\mathrm{ac}\) compares, \(\mathrm{ar1}\) and \(\mathrm{ar2}\) restore, \(\mathrm{amv}\) and \(\mathrm{asep}\) move the entry to \(W\)); \(\mathrm{ab}(f)\) moves \(W\) back (and, when no match was found, pushes a separator), and \(\mathrm{ad2}\), \(\mathrm{ad3}\) copy the name onto \(V\). For the diamonds, \(\mathrm{b0}\), \(\mathrm{b1}\) set \(P\); \(\mathrm{h0}\) takes the next entry; \(\mathrm{h1}\) to \(\mathrm{h5}\) set \(N\); \(\mathrm{r0}\) to \(\mathrm{r4}\) run the row loop, with \(\mathrm{wi}\) advancing \(R\); \(\mathrm{e0}\) to \(\mathrm{e2}\) set \(D\); \(\mathrm{dw}(p_p, p_n)\) walks \(F\) with the clause flags, \(\mathrm{dk}\), \(\mathrm{dr1}\), \(\mathrm{dr2}\), \(\mathrm{dm}\), \(\mathrm{dl}\) handle a literal with match bit \(b\), and \(\mathrm{dj}\) ends a clause; \(\mathrm{t0}\) moves \(T\) back to \(F\), and \(\mathrm{t1}\) to \(\mathrm{t8}\) drop the entry and advance \(P\). The labels \(\mathrm{z0}\) to \(\mathrm{z9}\) produce the output, and \(\mathrm{cpA}(j, b)\), \(\mathrm{cpB}(j, b)\), \(\mathrm{post}(j, b)\) copy site \(j\), passing \(b\) on.

inductive Lab
  | a0 | anm | aw (f : Bool) | ac (f : Bool) | ar1 (f : Bool) | ar2 (f : Bool) | amv (f : Bool)
  | asep (f : Bool) | ab (f : Bool) | ad2 | ad3
  | b0 | b1 | h0 | h1 | h2 | h3 | h4 | h5 | r0 | r1 | r2 | r3 | r4 | wi | e0 | e1 | e2
  | dw (pp pn : Bool) | dk (pp pn : Bool) | dr1 (pp pn b : Bool) | dr2 (pp pn b : Bool)
  | dm (pp pn b : Bool) | dl (pp pn b : Bool) | dj
  | t0 | t1 | t2 | t3 | t4 | t5 | t6 | t7 | t8
  | z0 | z1 | z2 | z3 | z4 | z5 | z6 | z7 | z8 | z9
  | cpA (j : Site) (b : Bool) | cpB (j : Site) (b : Bool) | post (j : Site) (b : Bool) | done
  deriving DecidableEq

Uses 1 · Used by 34

Statement usesCopy sites of the HAMPATH emitter

Used byLabel after a HAMPATH copy site · HAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Copy sites chained in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · End of a clause in the detour walk · Comparing a name with the top entry of the variable stack · Copying a counter in the HAMPATH emitter · The HAMPATH emitter machine · Run of a HAMPATH copy site · Start label of the HAMPATH emitter · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · Draining a counter · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time

DefinitionThe four pairs of Booleans#✓fully proved

The list of all pairs of Booleans in the order \((\mathrm{true}, \mathrm{true})\), \((\mathrm{true}, \mathrm{false})\), \((\mathrm{false}, \mathrm{true})\), \((\mathrm{false}, \mathrm{false})\).

def bb : List (Bool × Bool) := [(true, true), (true, false), (false, true), (false, false)]

Used by 1

Used bySAT ≤ HAMPATH is polynomial-time

DefinitionLabel after a HAMPATH copy site#✓fully proved

For a copy site \(j\) and a bit \(b\), the label that follows \(j\) is \(\mathrm{cpA}(j', b)\), where \(j'\) is the site after \(j\) in one of the chains \(f_{1u}, f_{1v}, f_{2u}, f_{2v}, f_{3u}, f_{3v}, f_{4u}, f_{4v}\), or \(w_{1u}, w_{1v}, w_{2u}, w_{2v}\), or \(d_{1u}, d_{1v}, d_{2u}, d_{2v}\), or \(d_{3u}, d_{3v}, d_{4u}, d_{4v}\). At the ends of the chains it is \(\mathrm{r0}\) after \(f_{4v}\), \(\mathrm{wi}\) after \(w_{2v}\) and \(\mathrm{dj}\) after \(d_{4v}\), whatever \(b\) is; after \(d_{2v}\) it is \(\mathrm{cpA}(d_{3u}, \mathrm{false})\) if \(b\) is true and \(\mathrm{dj}\) if \(b\) is false.

Cslib.Complexity.Karp.EmitHam.Site.nxt · 21 lines

def Site.nxt : Site → Bool → Lab
  | .f1u, b => .cpA .f1v b
  | .f1v, b => .cpA .f2u b
  | .f2u, b => .cpA .f2v b
  | .f2v, b => .cpA .f3u b
  | .f3u, b => .cpA .f3v b
  | .f3v, b => .cpA .f4u b
  | .f4u, b => .cpA .f4v b
  | .f4v, _ => .r0
  | .w1u, b => .cpA .w1v b
  | .w1v, b => .cpA .w2u b
  | .w2u, b => .cpA .w2v b
  | .w2v, _ => .wi
  | .d1u, b => .cpA .d1v b
  | .d1v, b => .cpA .d2u b
  | .d2u, b => .cpA .d2v b
  | .d2v, b => if b then .cpA .d3u false else .dj
  | .d3u, b => .cpA .d3v b
  | .d3v, b => .cpA .d4u b
  | .d4u, b => .cpA .d4v b
  | .d4v, _ => .dj

Uses 2 · Used by 4

Statement usesLabels of the HAMPATH emitter · Copy sites of the HAMPATH emitter

Used byCopy sites chained in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · The HAMPATH emitter machine · Run of a HAMPATH copy site

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.