structure Hex.GraphIso.Nauty.Sparse.ActiveScan {n : Nat} (active : VSet n) (queue : Array Nat) (next : Option Nat) : Prop

The initial active scan enumerates distinct members in ascending order; next is the least member not yet in the queue.

• ordered : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) queue.toList
• member (v : Nat) : v ∈ queue.toList → active.mem v = true
• next_mem (v : Nat) : next = some v → active.mem v = true
• ahead (v : Nat) : next = some v → ∀ (u : Nat), u ∈ queue.toList → u < v
• progress (v : Nat) : next = some v → queue.size ≤ v
• covers (v : Nat) : active.mem v = true → v ∈ queue.toList ∨ ∃ (w : Nat), next = some w ∧ w ≤ v

theorem Hex.GraphIso.Nauty.Sparse.ActiveScan.initial {n : Nat} (active : VSet n) : ActiveScan active #[] (active.nextElem none)

theorem Hex.GraphIso.Nauty.Sparse.ActiveScan.step {n i : Nat} {active : VSet n} {queue : Array Nat} {next : Option Nat} (h : ActiveScan active queue next) (hn : next = some i) : ActiveScan active (queue.push i) (active.nextElem (some i))

theorem Hex.GraphIso.Nauty.Sparse.ActiveScan.size_le {n : Nat} {active : VSet n} {queue : Array Nat} {next : Option Nat} (h : ActiveScan active queue next) : queue.size ≤ active.card

theorem Hex.GraphIso.Nauty.Sparse.ActiveScan.exhausted {n : Nat} {active : VSet n} {queue : Array Nat} {next : Option Nat} (h : ActiveScan active queue next) (hs : n ≤ queue.size) : next = none

Consuming n distinct bounded entries leaves no next member.

theorem Hex.GraphIso.Nauty.Sparse.ActiveScan.complete {n : Nat} {active : VSet n} {queue : Array Nat} {next : Option Nat} (h : ActiveScan active queue next) (hn : next = none) (v : Nat) : v ∈ queue.toList ↔ active.mem v = true