structure Hex.GraphIso.Nauty.Sparse.Index.Two (n first v2 v3 upto : Nat) (lab starts : Array Nat) : Prop

The first minimum fragment is indexed; the scatter of the second fragment is complete up to upto.

• size : starts.size = n
• minimum (q : Nat) : first ≤ q → q < v2 → starts[lab[q]!]! = if v2 = first + 1 then n else first
• second (q : Nat) : v2 ≤ q → q < upto → starts[lab[q]!]! = if v3 = v2 + 1 then n else v2

theorem Hex.GraphIso.Nauty.Sparse.Index.Two.initial {n first v2 v3 : Nat} {lab starts : Array Nat} (hs : starts.size = n) (hb : v2 ≤ n) (hbound : ∀ (i : Nat), i < n → lab[i]! < n) (hi : ∀ (q : Nat), first ≤ q → q < v2 → starts[lab[q]!]! = first) : Two n first v2 v3 v2 lab (if v2 = first + 1 then starts.setIfInBounds lab[first]! n else starts)

theorem Hex.GraphIso.Nauty.Sparse.Index.Two.step {n first v2 v3 upto : Nat} {lab starts : Array Nat} (h : Two n first v2 v3 upto lab starts) (hbound : ∀ (i : Nat), i < n → lab[i]! < n) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hu : v2 ≤ upto) (hb : upto < n) : Two n first v2 v3 (upto + 1) lab (starts.setIfInBounds lab[upto]! (if v3 = v2 + 1 then n else v2))

theorem Hex.GraphIso.Nauty.Sparse.Index.Two.step_long {n first v2 v3 upto : Nat} {lab starts : Array Nat} (h : Two n first v2 v3 upto lab starts) (hbound : ∀ (i : Nat), i < n → lab[i]! < n) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hu : v2 ≤ upto) (hb : upto < n) (hv : v3 ≠ v2 + 1) : Two n first v2 v3 (upto + 1) lab (starts.setIfInBounds lab[upto]! v2)

theorem Hex.GraphIso.Nauty.Sparse.Index.Two.relabel {n first v2 v3 upto : Nat} {lab starts out : Array Nat} (h : Two n first v2 v3 upto lab starts) (hv : v2 ≤ v3) (hu : upto ≤ v3) (hl : ∀ (q : Nat), q < v3 → out[q]! = lab[q]!) : Two n first v2 v3 upto out starts

theorem Hex.GraphIso.Nauty.Sparse.Index.Two.runs {n first v2 v3 : Nat} {lab starts ends hits : Array Nat} {last w1 w2 : Nat} (h : Two n first v2 v3 v3 lab starts) (hm : Minima lab hits first v2 v3 last w1 w2) (hv : v2 < v3) (hb : last ≤ n) (he : ends.size = n) : Runs n first (last - 1) v3 lab hits starts ((ends.setIfInBounds first (v2 - 1)).setIfInBounds v2 (v3 - 1))

The endpoint writes install precisely the first two maximal count runs.