def Hex.GraphIso.Nauty.After (cursor : Option Nat) (v : Nat) : Prop

Vertices strictly after the loop cursor.

Equations

• Hex.GraphIso.Nauty.After none v = True
• Hex.GraphIso.Nauty.After (some u) v = (u < v)

def Hex.GraphIso.Nauty.ChildLive {n : Nat} (rsLab : Array Nat) (tc len : Nat) (tcell : VSet n) (cursor : Option Nat) (o : Nat) : Prop

Offset o is still eligible after the loop cursor.

Equations

• Hex.GraphIso.Nauty.ChildLive rsLab tc len tcell cursor o = (o < len ∧ tcell.mem rsLab[tc + o]! = true ∧ Hex.GraphIso.Nauty.After cursor rsLab[tc + o]!)

theorem Hex.GraphIso.Nauty.after_or_not (cursor : Option Nat) (v : Nat) : After cursor v ∨ ¬After cursor v

Cursor eligibility is decidable without asking typeclass search to reduce the opaque After definition.

theorem Hex.GraphIso.Nauty.no_child_after {n : Nat} {s : VSet n} {cursor : Option Nat} (hnext : s.nextElem cursor = none) (v : Nat) : s.mem v = true → After cursor v → False

A none cursor result means that no set member remains after the cursor.

theorem Hex.GraphIso.Nauty.nextElem_after {n : Nat} {s : VSet n} {v : Nat} {cursor : Option Nat} (hnext : s.nextElem cursor = some v) : After cursor v

A successful nextElem lies strictly after its cursor.

theorem Hex.GraphIso.Nauty.nextElem_le {n : Nat} {s : VSet n} {v w : Nat} {cursor : Option Nat} (hnext : s.nextElem cursor = some v) (hw : s.mem w = true) (ha : After cursor w) : v ≤ w

nextElem returns the least set member strictly after its cursor.

theorem Hex.GraphIso.Nauty.worksetOf_eq_windowSet {n : Nat} (lab : Array Nat) (tc len : Nat) (hlen : 1 ≤ len) : worksetOf n lab tc (tc + len - 1) = windowSet n lab tc len

The target-cell representation used by maketargetcell is the same bitset as the length-indexed window representation used by sweep coverage.

theorem Hex.GraphIso.Nauty.nextElem_windowSet_some {n : Nat} {lab : Array Nat} {tc len : Nat} (hlen : 1 ≤ len) (hlt : lab[tc]! < n) : ∃ (v : Nat), (windowSet n lab tc len).nextElem none = some v

The start of a sweep always has a first vertex.