theorem Hex.GraphIso.Nauty.Sparse.replace_perm (queue : Array Nat) (pos v : Nat) (hp : pos < queue.size) : (queue.setIfInBounds pos v).toList.Perm (queue.toList.erase queue[pos]! ++ [v])

Replacing a queue slot changes precisely its selected occurrence.

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

theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.replace {n pos v : Nat} {active : VSet n} {queue : Array Nat} (h : ActiveQueue active queue) (hp : pos < queue.size) (hv : v < n) (hf : active.mem v = false) : ActiveQueue ((active.erase queue[pos]!).insert v) (queue.setIfInBounds pos v)

The largest-fragment replacement preserves the exact active set when the replacement first cell was inactive.