def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.base {n : Nat} (s : Control n) (distance : Bool) (first w1 w2 v2 : Nat) : Control n

Equations

• s.base distance first w1 w2 v2 = ((s.hash first).hash (if distance = true then w2 else w1)).hash v2

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.pair {n : Nat} (s : Control n) (first v2 v3 : Nat) : Control n

Equations

• s.pair first v2 v3 = if (decide (v2 - first ≤ v3 - v2) && !s.active.mem first) = true then s.push first else s.push v2

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.more {n : Nat} (s : Control n) (distance : Bool) (first v2 v3 : Nat) : Control n × Option Nat × Nat

The first tail state, after the second fragment has been enqueued and the initial largest-fragment comparison has executed.

Equations

• One or more equations did not get rendered due to their size.

inductive Hex.GraphIso.Nauty.Sparse.CountTrace.Result {n : Nat} (distance : Bool) (first last : Nat) (s : RefineSt n) (lab : Array Nat) : Control n → Prop

The complete control trace of a count split: uniform early return, two fragments, or the first two fragments followed by the tail derivation.

• uniform {n : Nat} {distance : Bool} {first last : Nat} {s : RefineSt n} {lab : Array Nat} (hu : ∀ (q : Nat), first ≤ q → q < last → s.hits[s.lab[q]!]! = s.hits[s.lab[first]!]!) : Result distance first last s lab ((control s).hash first)
• divided {n : Nat} {distance : Bool} {first last : Nat} {s : RefineSt n} {lab : Array Nat} {v2 v3 w1 w2 : Nat} {out : Control n} (hn : ∃ (q : Nat), first ≤ q ∧ q < last ∧ s.hits[s.lab[q]!]! ≠ s.hits[s.lab[first]!]!) (hm : Minima lab s.hits first v2 v3 last w1 w2) (hv : v2 < v3) (hc : if v3 = last then out = ((control s).base distance first w1 w2 v2).pair first v2 v3 else let c := ((control s).base distance first w1 w2 v2).more distance first v2 v3; Tail distance lab s.hits first last (v3 - 1) c.fst c.snd.fst c.snd.snd out) : Result distance first last s lab out