theorem Hex.GraphIso.Nauty.Sparse.reach_advance {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (reachContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st out : State n) (exit : Generic.Exit) (hl : 1 ≤ level) (h : Ready G level numcells st) (htarget : Generic.Target State.frame level tc cell st) (hx : FrameOut G level level st out) : FrameOut G level level st (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd

Recovery and both target filters preserve the parent frame before the next surviving sibling. Filters need only be subsets for this reachability rule.

theorem Hex.GraphIso.Nauty.Sparse.reach_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {descend : Generic.NodeFn (State n)} {next : Generic.SweepFn (State n) n} (hdescend : (reachContract G).nodeValid fuel descend) (hnext : (reachContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : Ready G level numcells st) (htarget : Generic.Target State.frame level tc cell st) (htv : cell.mem tv = true) : FrameOut G level level st (Generic.sweepStep (n + 2) descend next first level numcells tc tv1 tv cell index st).snd.snd

The executed sparse sweep individualizes only a member of its current target cell and composes every recursive return with its caller's frame.