theorem Hex.GraphIso.Nauty.Sparse.Store.target {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (first : Bool) (tcLevel level numcells : Nat) : Store G (chooseTarget first (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.Store.recover {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (inf level : Nat) : Store G (Generic.Policy.recover inf level st)

theorem Hex.GraphIso.Nauty.Sparse.Store.push {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (pair : VSet n × VSet n) : Store G (pushAuto st pair)

theorem Hex.GraphIso.Nauty.Sparse.Store.admit {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) : Store G (Nauty.admit st)

theorem Hex.GraphIso.Nauty.Sparse.Store.prune {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level : Nat) : Store G (pruneReturn level st).snd

theorem Hex.GraphIso.Nauty.Sparse.Store.leaf {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (leaf : Leaf) (level : Nat) (hc : ∀ (sr : Nat), leaf = Generic.Leaf.better sr → Candidate G st sr) : Store G (leafExit leaf level st).snd

All five shared leaf actions preserve the native store; only a better leaf replaces its label, using the prefix supplied by classification.