theorem Hex.GraphIso.Nauty.Sparse.refine_loop_equiv {n : 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) (level : Nat) (s t : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (he : RefineSt.Equiv (renamingOf p) level s t) : have run := fun (g : Graph n) (s : RefineSt n) => (have s := s; do let __s ← forIn [:n] s fun (x : Nat) (__s : RefineSt n) => have s := __s; if (s.queue.isEmpty || decide (s.numcells ≥ n)) = true then pure (ForInStep.done s) else have pos := s.queue.size - 1; do let __s ← forIn [:min s.queue.size 10] pos fun (i __s : Nat) => have pos := __s; if s.ptn[s.queue[i]!]! ≤ level then have pos := i; pure (ForInStep.done pos) else pure (ForInStep.yield pos) have pos : Nat := __s have split : Nat := s.queue[pos]! have queue : Array Nat := (s.queue.set! pos s.queue[s.queue.size - 1]!).pop have s : RefineSt n := { lab := s.lab, ptn := s.ptn, active := s.active.erase split, queue := queue, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode } have s : RefineSt n := s.hash split if s.ptn[split]! ≤ level then have s := splitSingleton g level split s; pure (ForInStep.yield s) else have s := splitNontrivial g level split s; pure (ForInStep.yield s) have s : RefineSt n := __s pure s).run; RefineSt.Equiv (renamingOf p) level (run (Graph.ofGraph G) s) (run (Graph.ofGraph H) t)

The full literal main refinement loop transports its observations, including both stopping guards, first-ten preference, swap/pop removal, hashing and both native splitter branches.