theorem Hex.GraphIso.Nauty.Sparse.binary_step {n : Nat} (level first stamp : Nat) (s : RefineSt n) (hf : first ≤ s.cellend[first]! + 1) (hb : s.cellend[first]! + 1 ≤ s.lab.size) (hstarts : s.cellstart.size = n) (hvertices : ∀ (v : Nat), v ∈ s.lab.toList → v < n) : have last := s.cellend[first]! + 1; have pred := fun (v : Nat) => s.vmarks[v]! == stamp; have r := (have s := s.hash first; have last := s.cellend[first]! + 1; have lab := s.lab; have s := { lab := #[], ptn := s.ptn, active := s.active, queue := s.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 v2 := first; have hit := #[]; do let __s ← forIn [first:last] (lab, v2, hit) fun (j : Nat) (__s : Array Nat × Nat × Array Nat) => have lab := __s.fst; have __s := __s.snd; have v2 := __s.fst; have hit := __s.snd; have v := lab[j]!; if (s.vmarks[v]! == stamp) = true then have hit := hit.push v; pure (ForInStep.yield (lab, v2, hit)) else have lab := lab.set! v2 v; have v2 := v2 + 1; pure (ForInStep.yield (lab, v2, hit)) have lab : Array Nat := __s.fst have __s : Nat × Array Nat := __s.snd have v2 : Nat := __s.fst have hit : Array Nat := __s.snd have s : RefineSt n := s.hash hit.size have starts : Array Nat := s.cellstart have s : RefineSt n := { lab := s.lab, ptn := s.ptn, active := s.active, queue := s.queue, 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 v3 : Nat := v2 let __s ← forIn [:hit.size] (lab, starts, v3) fun (t : Nat) (__s : Array Nat × Array Nat × Nat) => have lab := __s.fst; have __s := __s.snd; have starts := __s.fst; have v3 := __s.snd; have j := hit[hit.size - 1 - t]!; have starts := starts.set! j v2; have lab := lab.set! v3 j; have v3 := v3 + 1; pure (ForInStep.yield (lab, starts, v3)) have lab : Array Nat := __s.fst have __s : Array Nat × Nat := __s.snd have starts : Array Nat := __s.fst have v3 : Nat := __s.snd have __do_jp : PUnit → RefineSt n → Array Nat → Id (RefineSt n) := fun (__r : PUnit) (s : RefineSt n) (starts : Array Nat) => pure { lab := lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := starts, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode } if (v2 != v3 && v2 != first) = true then have __do_jp := fun (__r : PUnit) (starts : Array Nat) => have __do_jp := fun (__r : PUnit) (starts : Array Nat) => have s := { lab := s.lab, ptn := s.ptn.set! (v2 - 1) level, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := (s.cellend.set! first (v2 - 1)).set! v2 (v3 - 1), indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells + 1, longcode := s.longcode }; have s := s.hash v2; if (decide (v2 - first ≤ v3 - v2) && !s.active.mem first) = true then have s := s.push first; __do_jp PUnit.unit s starts else have s := s.push v2; __do_jp PUnit.unit s starts; if (v3 == v2 + 1) = true then have starts := starts.set! lab[v2]! n; __do_jp PUnit.unit starts else __do_jp PUnit.unit starts; if (v2 == first + 1) = true then have starts := starts.set! lab[first]! n; __do_jp PUnit.unit starts else __do_jp PUnit.unit starts else __do_jp PUnit.unit s starts).run; Binary.Cell level first last pred s r

One executed singleton-cell body has the control, partition and counter specified by its number of marked and unmarked input vertices.