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

Every active queue entry is the beginning of a partition cell, and the queue agrees exactly with the packed active set.

• set : ActiveQueue active queue
• starts (v : Nat) : active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.of_scan {n level : Nat} {ptn queue : Array Nat} {active : VSet n} (h : ActiveScan active queue none) (hs : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) : CellQueue ptn level active queue

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.fresh {n level v : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hv : 0 < v) (ho : level < ptn[v - 1]!) : active.mem v = false

An open interior position cannot already be an active cell start.

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.partition {n level : Nat} {ptn after queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hc : ∀ (q : Nat), ptn[q]! ≤ level → after[q]! ≤ level) : CellQueue after level active queue

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.cut {n level : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (q : Nat) : CellQueue (ptn.setIfInBounds q level) level active queue

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.push {n level v : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hv : v < n) (hs : v = 0 ∨ ptn[v - 1]! ≤ level) (hf : active.mem v = false) : CellQueue ptn level (active.insert v) (queue.push v)

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.cut_push {n level v : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hv : 0 < v) (hn : v < n) (hb : v - 1 < ptn.size) (ho : level < ptn[v - 1]!) : CellQueue (ptn.setIfInBounds (v - 1) level) level (active.insert v) (queue.push v)

A new interior cut creates a fresh active cell start.

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.cut_next {n level : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (q : Nat) (hn : q + 1 < n) (hb : q < ptn.size) (ho : level < ptn[q]!) : CellQueue (ptn.setIfInBounds q level) level (active.insert (q + 1)) (queue.push (q + 1))

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.remove {n level pos : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hp : pos < queue.size) : CellQueue ptn level (active.erase queue[pos]!) (queue.setIfInBounds pos queue[queue.size - 1]!).pop

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.replace {n level v pos : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hp : pos < queue.size) (hv : v < n) (hs : v = 0 ∨ ptn[v - 1]! ≤ level) (hf : active.mem v = false) : CellQueue ptn level ((active.erase queue[pos]!).insert v) (queue.setIfInBounds pos v)

theorem Hex.GraphIso.Nauty.Sparse.CellQueue.replace_get {n level v pos : Nat} {ptn queue : Array Nat} {active : VSet n} (h : CellQueue ptn level active queue) (hp : pos < queue.size) (hv : v < n) (hs : v = 0 ∨ ptn[v - 1]! ≤ level) (hf : active.mem v = false) : CellQueue ptn level ((active.erase queue[pos]).insert v) (queue.setIfInBounds pos v)