theorem Hex.GraphIso.Nauty.Sparse.take_set (lab : Array Nat) (k v : Nat) (hk : k < lab.size) : List.take (k + 1) (lab.setIfInBounds k v).toList = List.take k lab.toList ++ [v]

A write at the end of a retained prefix appends exactly that vertex.

structure Hex.GraphIso.Nauty.Sparse.Compact (before : Array Nat) (p : Nat → Bool) (first upto : Nat) (seen : List Nat) (lab hit : Array Nat) (next : Nat) : Prop

The singleton splitter compacts the vertices that do not meet the splitter while collecting the others. Unread source positions are retained.

• bounds : first ≤ next ∧ next ≤ upto ∧ upto ≤ before.size
• size : lab.size = before.size
• count : next = first + (List.filter (fun (v : Nat) => !p v) seen).length
• kept : List.take next lab.toList = List.take first before.toList ++ List.filter (fun (v : Nat) => !p v) seen
• hits : hit.toList = List.filter p seen
• exterior (q : Nat) : q < before.size → q < first ∨ upto ≤ q → lab[q]! = before[q]!

theorem Hex.GraphIso.Nauty.Sparse.Compact.initial (before : Array Nat) (p : Nat → Bool) (first : Nat) (hb : first ≤ before.size) : Compact before p first first [] before #[] first

theorem Hex.GraphIso.Nauty.Sparse.Compact.collect {before : Array Nat} {p : Nat → Bool} {first upto : Nat} {seen : List Nat} {lab hit : Array Nat} {next : Nat} (h : Compact before p first upto seen lab hit next) (hb : upto < before.size) (hv : p before[upto]! = true) : Compact before p first (upto + 1) (seen ++ [before[upto]!]) lab (hit.push before[upto]!) next

theorem Hex.GraphIso.Nauty.Sparse.Compact.keep {before : Array Nat} {p : Nat → Bool} {first upto : Nat} {seen : List Nat} {lab hit : Array Nat} {next : Nat} (h : Compact before p first upto seen lab hit next) (hb : upto < before.size) (hv : p before[upto]! = false) : Compact before p first (upto + 1) (seen ++ [before[upto]!]) (lab.setIfInBounds next before[upto]!) hit (next + 1)