theorem Hex.GraphIso.Nauty.Sparse.refineWith_state {n : Nat} (G : SparseGraph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) (hb : Scratch.Bounded n scratch) : have t := refineWith (Graph.ofGraph G) level lab ptn active numcells scratch; t.lab.toList.Perm (List.range n) ∧ t.ptn.size = n ∧ Cuts level n ptn t.ptn numcells t.numcells n ∧ cellsPerm ptn level t.lab lab ∧ CellQueue t.ptn level t.active t.queue ∧ Scratch.Valid n t.lab t.ptn level t.toScratch

Full refinement retains labels, original cell contents and boundaries, exact cell accounting, a valid cache, and the active queue invariant.