structure Hex.GraphIso.Nauty.Sparse.Scan {n : Nat} (G : SparseGraph n) (root : Fin n) (dist queue : Array Nat) (head tail current next : Nat) (seen : List Nat) extends Hex.GraphIso.Nauty.Sparse.Bfs G root dist queue head tail : Prop

State of one packed adjacency scan. The queue head is advanced only after all these edge obligations have been discharged.

• dist_size : dist.size = n
• queue_size : queue.size = n
• head_le : head ≤ tail
• tail_le : tail ≤ n
• vertex (i : Nat) : i < tail → queue[i]! < n
• injective (i j : Nat) : i < tail → j < tail → queue[i]! = queue[j]! → i = j
• bound (v : Nat) : v < n → dist[v]! ≤ n
• found (v : Nat) : v < n → (dist[v]! < n ↔ ∃ (i : Nat), i < tail ∧ queue[i]! = v)
• index (i : Nat) : i < tail → dist[queue[i]!]! ≤ i
• sorted (i j : Nat) : i ≤ j → j < tail → dist[queue[i]!]! ≤ dist[queue[j]!]!
• band (i j : Nat) : head ≤ i → i < tail → j < tail → dist[queue[j]!]! ≤ dist[queue[i]!]! + 1
• root_eq : dist[↑root]! = 0
• sound (v : Nat) (hv : v < n) : dist[v]! < n → Walk G root ⟨v, hv⟩ dist[v]!
• edges (i : Nat) (hi : i < head) (v : Fin n) : G.adj ⟨queue[i]!, ⋯⟩ v = true → dist[↑v]! < n ∧ dist[↑v]! ≤ dist[queue[i]!]! + 1
• head_lt : head < tail
• head_eq : queue[head]! = current
• next_eq : dist[current]! + 1 = next
• next_lt : next < n
• visited (e : Nat) : e ∈ seen → dist[(Graph.ofGraph G).neighbor e]! < n ∧ dist[(Graph.ofGraph G).neighbor e]! ≤ next

theorem Hex.GraphIso.Nauty.Sparse.Scan.current_lt {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail current next : Nat} {seen : List Nat} (h : Scan G root dist queue head tail current next seen) : current < n

theorem Hex.GraphIso.Nauty.Sparse.Scan.current_finite {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail current next : Nat} {seen : List Nat} (h : Scan G root dist queue head tail current next seen) : dist[current]! < n

theorem Hex.GraphIso.Nauty.Sparse.Scan.initial {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail : Nat} (h : Bfs G root dist queue head tail) (hh : head < tail) (ht : tail < n) : Scan G root dist queue head tail queue[head]! (dist[queue[head]!]! + 1) []

theorem Hex.GraphIso.Nauty.Sparse.Scan.add {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail current next e : Nat} {seen : List Nat} (h : Scan G root dist queue head tail current next seen) (hlo : G.offsets[current]! ≤ e) (hhi : e < G.offsets[current + 1]!) (hd : dist[(Graph.ofGraph G).neighbor e]! = n) : Scan G root (dist.set! ((Graph.ofGraph G).neighbor e) next) (queue.set! tail ((Graph.ofGraph G).neighbor e)) head (tail + 1) current next (seen ++ [e])

theorem Hex.GraphIso.Nauty.Sparse.Scan.keep {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail current next e : Nat} {seen : List Nat} (h : Scan G root dist queue head tail current next seen) (hhi : e < G.offsets[current + 1]!) (hd : dist[(Graph.ofGraph G).neighbor e]! ≠ n) : Scan G root dist queue head tail current next (seen ++ [e])

theorem Hex.GraphIso.Nauty.Sparse.Scan.finish {n : Nat} {G : SparseGraph n} {root : Fin n} {dist queue : Array Nat} {head tail current next : Nat} (h : Scan G root dist queue head tail current next (List.range' G.offsets[current]! (G.offsets[current + 1]! - G.offsets[current]!))) : Bfs G root dist queue (head + 1) tail