def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.binary {n : Nat} (c : Control n) (first cut last : Nat) : Control n

Control at the singleton splitter's conditional fragment finalization. Uniform predicate classes do not close a boundary or enqueue a fragment.

Equations

• c.binary first cut last = if cut ≠ last ∧ cut ≠ first then (c.hash cut).pair first cut last else c

structure Hex.GraphIso.Nauty.Sparse.Binary.Result {n : Nat} (level first cut last : Nat) (s : RefineSt n) (lab starts : Array Nat) (r : RefineSt n) : Prop

Observations of conditional binary-fragment finalization, including its exact label and index writes and unchanged scratch storage.

• control : CountTrace.control r = (CountTrace.control s).binary first cut last
• ptn : r.ptn = if cut ≠ last ∧ cut ≠ first then s.ptn.set! (cut - 1) level else s.ptn
• count : r.numcells = if cut ≠ last ∧ cut ≠ first then s.numcells + 1 else s.numcells
• label : r.lab = lab
• starts_eq : r.cellstart = if cut ≠ last ∧ cut ≠ first then let middle := if cut = first + 1 then starts.set! lab[first]! n else starts; if last = cut + 1 then middle.set! lab[cut]! n else middle else starts
• ends : r.cellend = if cut ≠ last ∧ cut ≠ first then (s.cellend.set! first (cut - 1)).set! cut (last - 1) else s.cellend
• frame : CountFrame { 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 } r

theorem Hex.GraphIso.Nauty.Sparse.binary_control {n : Nat} (level first cut last : Nat) (s : RefineSt n) (lab starts : Array Nat) : have r := (have s := s; have starts := starts; have __do_jp := 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 (cut != last && cut != 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! (cut - 1) level, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := (s.cellend.set! first (cut - 1)).set! cut (last - 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 cut; if (decide (cut - first ≤ last - cut) && !s.active.mem first) = true then have s := s.push first; __do_jp PUnit.unit s starts else have s := s.push cut; __do_jp PUnit.unit s starts; if (last == cut + 1) = true then have starts := starts.set! lab[cut]! n; __do_jp PUnit.unit starts else __do_jp PUnit.unit starts; if (cut == 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.Result level first cut last s lab starts r

The singleton splitter's actual endpoint, sentinel, hash and queue finalization has the stated observations; the label and cache arrays keep their executed representation and ownership transfers.