def Hex.GraphIso.Nauty.Sparse.Binary.seen (lab : Array Nat) (first last : Nat) : List Nat

The input vertices traversed by one singleton-cell scan.

Equations

• Hex.GraphIso.Nauty.Sparse.Binary.seen lab first last = List.map (fun (q : Nat) => lab[q]!) (List.range' first (last - first))

def Hex.GraphIso.Nauty.Sparse.Binary.hits (lab : Array Nat) (pred : Nat → Bool) (first last : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.Sparse.Binary.hits lab pred first last = (List.filter pred (Hex.GraphIso.Nauty.Sparse.Binary.seen lab first last)).length

def Hex.GraphIso.Nauty.Sparse.Binary.cut (lab : Array Nat) (pred : Nat → Bool) (first last : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.Sparse.Binary.cut lab pred first last = first + (List.filter (fun (v : Nat) => !pred v) (Hex.GraphIso.Nauty.Sparse.Binary.seen lab first last)).length

theorem Hex.GraphIso.Nauty.Sparse.Binary.seen_eq (lab : Array Nat) (first last : Nat) : seen lab first last = segN lab first (last - first)

structure Hex.GraphIso.Nauty.Sparse.Binary.Cell {n : Nat} (level first last : Nat) (pred : Nat → Bool) (s t : RefineSt n) : Prop

Observations of one complete executed singleton-cell body. The cut and hit count refer to its input traversal; the loop theorem derives every field from the executed compaction, reverse fill and finalization.

• control : CountTrace.control t = (((CountTrace.control s).hash first).hash (hits s.lab pred first last)).binary first (cut s.lab pred first last) last
• ptn : t.ptn = if cut s.lab pred first last ≠ last ∧ cut s.lab pred first last ≠ first then s.ptn.set! (cut s.lab pred first last - 1) level else s.ptn
• count : t.numcells = if cut s.lab pred first last ≠ last ∧ cut s.lab pred first last ≠ first then s.numcells + 1 else s.numcells
• frame : CountFrame s t
• window : «Sort».Window s.lab t.lab first last
• retained : segN t.lab first (cut s.lab pred first last - first) = List.filter (fun (v : Nat) => !pred v) (seen s.lab first last)
• collected : segN t.lab (cut s.lab pred first last) (last - cut s.lab pred first last) = (List.filter pred (seen s.lab first last)).reverse
• cache : s.lab.toList.Perm (List.range n) → s.ptn.size = n → Index.Valid n s.lab s.ptn level s.cellstart s.cellend → IsCell s.ptn level first (last - first) → first + 1 < last → Index.Valid n t.lab t.ptn level t.cellstart t.cellend