theorem Hex.GraphIso.Nauty.Sparse.prefix_read {lab : Array Nat} {pre data : List Nat} {upto q : Nat} (h : List.take upto lab.toList = pre ++ data) (hq : pre.length ≤ q) (hu : q < upto) (hb : q < lab.size) : lab[q]! = data[q - pre.length]!

Read a copied list after a fixed array prefix.

theorem Hex.GraphIso.Nauty.Sparse.Fill.read {before : Array Nat} {data : List Nat} {first upto : Nat} {after : Array Nat} {q : Nat} (h : Fill before data first upto after) (hq : first ≤ q) (hu : q < first + upto) : after[q]! = data[q - first]!

theorem Hex.GraphIso.Nauty.Sparse.Compact.retained {before : Array Nat} {p : Nat → Bool} {first upto : Nat} {seen : List Nat} {lab hit : Array Nat} {next q : Nat} (h : Compact before p first upto seen lab hit next) (hq : first ≤ q) (hu : q < next) : p lab[q]! = false

Every vertex retained by compaction fails the split predicate.

theorem Hex.GraphIso.Nauty.Sparse.Compact.separated {before : Array Nat} {p : Nat → Bool} {first last : Nat} {seen : List Nat} {lab hit : Array Nat} {next : Nat} {out : Array Nat} (h : Compact before p first last seen lab hit next) (hlen : seen.length = last - first) (hr : Fill lab hit.toList.reverse next hit.toList.reverse.length out) : (∀ (q : Nat), first ≤ q → q < next → p out[q]! = false) ∧ ∀ (q : Nat), next ≤ q → q < last → p out[q]! = true

Reinsertion produces the two predicate classes in the required order.