structure Hex.GraphIso.Nauty.Sparse.Index.Writes (n : Nat) (before after : Array Nat) (vertices : List Nat) (value : Nat) : Prop

Vertex-index writes assign one value precisely to the vertices traversed. Repeated occurrences are harmless because the assigned value is fixed.

• size : after.size = n
• get (v : Nat) : v < n → after[v]! = if v ∈ vertices then value else before[v]!

theorem Hex.GraphIso.Nauty.Sparse.Index.Writes.initial {n : Nat} {before : Array Nat} {value : Nat} (h : before.size = n) : Writes n before before [] value

theorem Hex.GraphIso.Nauty.Sparse.Index.Writes.step {n : Nat} {before after : Array Nat} {vertices : List Nat} {value v : Nat} (h : Writes n before after vertices value) (hv : v < n) : Writes n before (after.setIfInBounds v value) (vertices ++ [v]) value

theorem Hex.GraphIso.Nauty.Sparse.Index.Writes.skip {n : Nat} {before after : Array Nat} {vertices : List Nat} {value v : Nat} (h : Writes n before after vertices value) (hv : n ≤ v) : Writes n before after (vertices ++ [v]) value

An out-of-range sentinel adds no writable vertex.

theorem Hex.GraphIso.Nauty.Sparse.Index.Writes.repeated {n : Nat} {before after : Array Nat} {vertices : List Nat} {value v : Nat} (h : Writes n before after vertices value) (hv : v ∈ vertices) : Writes n before after (vertices ++ [v]) value

Repeating a vertex already written does not change the scatter.