theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.singleton {n level : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) {s t : RefineSt n} (h : Equiv (renamingOf p) level s t) (hs : Valid level s) (ht : Valid level t) (split : Nat) (hb : split < n) (hc : IsCell s.ptn level split 1) : Equiv (renamingOf p) level (splitSingleton (Graph.ofGraph G) level split s) (splitSingleton (Graph.ofGraph H) level split t)

The native singleton branch transports at valid working states.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.nontrivial {n level : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) {s t : RefineSt n} (h : Equiv (renamingOf p) level s t) (hs : Valid level s) (ht : Valid level t) (split len : Nat) (hc : IsCell s.ptn level split len) (hb : split + len ≤ n) : Equiv (renamingOf p) level (splitNontrivial (Graph.ofGraph G) level split s) (splitNontrivial (Graph.ofGraph H) level split t)

The native nontrivial branch transports at valid working states.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.selected {n level : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) {s t : RefineSt n} (h : Equiv (renamingOf p) level s t) (hs : Valid level s) (ht : Valid level t) (pos : Nat) (hp : pos < s.queue.size) : Equiv (renamingOf p) level (RefineSt.selected (Graph.ofGraph G) level pos s) (RefineSt.selected (Graph.ofGraph H) level pos t)

The actual selected queue entry, swap/pop removal, hash and branch dispatch transport together.