theorem Hex.GraphIso.Nauty.Sparse.drop_eq {before after : Array Nat} {k : Nat} (hs : after.size = before.size) (he : ∀ (q : Nat), q < before.size → k ≤ q → after[q]! = before[q]!) : List.drop k after.toList = List.drop k before.toList

Pointwise agreement above a position identifies the complete suffix.

structure Hex.GraphIso.Nauty.Sparse.Fill (before : Array Nat) (data : List Nat) (first upto : Nat) (after : Array Nat) : Prop

Consecutive writes copy the prescribed list into an array while retaining its prefix and unread suffix.

• fits : first + data.length ≤ before.size
• bound : upto ≤ data.length
• size : after.size = before.size
• copied : List.take (first + upto) after.toList = List.take first before.toList ++ List.take upto data
• exterior (q : Nat) : q < first ∨ first + upto ≤ q → after[q]! = before[q]!

theorem Hex.GraphIso.Nauty.Sparse.Fill.initial (before : Array Nat) (data : List Nat) (first : Nat) (hb : first + data.length ≤ before.size) : Fill before data first 0 before

theorem Hex.GraphIso.Nauty.Sparse.Fill.step {before : Array Nat} {data : List Nat} {first upto : Nat} {after : Array Nat} (h : Fill before data first upto after) (hb : upto < data.length) : Fill before data first (upto + 1) (after.setIfInBounds (first + upto) data[upto]!)

theorem Hex.GraphIso.Nauty.Sparse.Fill.finish {before : Array Nat} {data : List Nat} {first : Nat} {after : Array Nat} (h : Fill before data first data.length after) : after.toList = List.take first before.toList ++ data ++ List.drop (first + data.length) before.toList

At completion all requested entries have been copied, with exact exterior contents. This applies to the singleton splitter's reverse hit reinsertion.