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

The mutable refinement queue enumerates the packed active set exactly once; its order is the order used by nauty's splitter selection.

• nodup : queue.toList.Nodup
• mem (v : Nat) : v ∈ queue.toList ↔ active.mem v = true

theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.of_scan {n : Nat} {active : VSet n} {queue : Array Nat} (h : ActiveScan active queue none) : ActiveQueue active queue

theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.bound {n v : Nat} {active : VSet n} {queue : Array Nat} (h : ActiveQueue active queue) (hv : v ∈ queue.toList) : v < n

theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.push {n v : Nat} {active : VSet n} {queue : Array Nat} (h : ActiveQueue active queue) (hv : v < n) (hf : active.mem v = false) : ActiveQueue (active.insert v) (queue.push v)

theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.erase {n v : Nat} {active : VSet n} {queue out : Array Nat} (h : ActiveQueue active queue) (hp : out.toList.Perm (queue.toList.erase v)) : ActiveQueue (active.erase v) out

Erasing a queue occurrence agrees with packed-set erasure because the queue contains no duplicates. The array removal may reorder other entries.