structure Hex.GraphIso.Nauty.Sparse.Index.Frame (n first last : Nat) (oldlab lab oldstarts starts oldends ends : Array Nat) : Prop

Cache entries outside the cell being split retain their old meaning.

• ends (q : Nat) : q < first ∨ last < q → ends[q]! = oldends[q]!
• starts (q : Nat) : q < n → q < first ∨ last < q → starts[lab[q]!]! = oldstarts[oldlab[q]!]!

theorem Hex.GraphIso.Nauty.Sparse.Index.Frame.of_window {n first last : Nat} {oldlab lab starts ends : Array Nat} (hw : «Sort».Window oldlab lab first (last + 1)) : Frame n first last oldlab lab starts starts ends ends

theorem Hex.GraphIso.Nauty.Sparse.Index.Frame.set_end {n first last a value : Nat} {oldlab lab oldstarts starts oldends ends : Array Nat} (h : Frame n first last oldlab lab oldstarts starts oldends ends) (ha : first ≤ a ∧ a ≤ last) : Frame n first last oldlab lab oldstarts starts oldends (ends.setIfInBounds a value)

theorem Hex.GraphIso.Nauty.Sparse.Index.Frame.set_start {n first last a value : Nat} {oldlab lab oldstarts starts oldends ends : Array Nat} (h : Frame n first last oldlab lab oldstarts starts oldends ends) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (ha : first ≤ a ∧ a ≤ last) (hb : a < n) : Frame n first last oldlab lab oldstarts (starts.setIfInBounds lab[a]! value) oldends ends

theorem Hex.GraphIso.Nauty.Sparse.Index.Frame.scatter {n first last a value : Nat} {oldlab lab oldstarts starts oldends ends out : Array Nat} {upto : Nat} (h : Frame n first last oldlab lab oldstarts starts oldends ends) (hs : Scatter n lab starts out a upto value) (ha : first ≤ a) (hb : upto ≤ last + 1) : Frame n first last oldlab lab oldstarts out oldends ends

theorem Hex.GraphIso.Nauty.Sparse.Index.Frame.relabel {n first last : Nat} {oldlab lab oldstarts starts oldends ends out : Array Nat} (h : Frame n first last oldlab lab oldstarts starts oldends ends) (hw : «Sort».Window lab out first (last + 1)) : Frame n first last oldlab out oldstarts starts oldends ends