structure Hex.GraphIso.Nauty.Sparse.Marks (n stamp : Nat) (a : Array Nat) (member : Nat → Prop) : Prop

The current generation marks exactly the specified vertices.

• size : a.size = n
• bound (v : Nat) : v < n → a[v]! ≤ stamp
• marked (v : Nat) : v < n → (a[v]! = stamp ↔ member v)

theorem Hex.GraphIso.Nauty.Sparse.Marks.fresh {n stamp : Nat} {a : Array Nat} (hs : a.size = n) (hb : ∀ (v : Nat), v < n → a[v]! < stamp) : Marks n stamp a fun (x : Nat) => False

theorem Hex.GraphIso.Nauty.Sparse.Marks.congr {n stamp : Nat} {a : Array Nat} {member : Nat → Prop} (h : Marks n stamp a member) {other : Nat → Prop} (he : ∀ (v : Nat), v < n → (member v ↔ other v)) : Marks n stamp a other

theorem Hex.GraphIso.Nauty.Sparse.Marks.set {n stamp : Nat} {a : Array Nat} {member : Nat → Prop} (h : Marks n stamp a member) {v : Nat} (hv : v < n) : Marks n stamp (a.set! v stamp) fun (w : Nat) => member w ∨ w = v

theorem Hex.GraphIso.Nauty.Sparse.Marks.clear {n stamp : Nat} {a : Array Nat} {member : Nat → Prop} (h : Marks n stamp a member) (hs : 0 < stamp) {v : Nat} (hv : v < n) : Marks n stamp (a.set! v 0) fun (w : Nat) => member w ∧ w ≠ v

structure Hex.GraphIso.Nauty.Sparse.Diff (n stamp : Nat) (old seen : List Nat) (a : Array Nat) (mina : Nat) : Prop

During candidate scanning, the live marks describe old-only vertices; mina is the least candidate-only vertex encountered, or the sentinel.

• marks : Marks n stamp a fun (v : Nat) => v ∈ old ∧ ¬v ∈ seen
• seen_lt (v : Nat) : v ∈ seen → v < n
• min_le : mina ≤ n
• witness : mina < n → mina ∈ seen ∧ ¬mina ∈ old
• least (v : Nat) : v ∈ seen → ¬v ∈ old → mina ≤ v

theorem Hex.GraphIso.Nauty.Sparse.Diff.initial {n stamp : Nat} {old : List Nat} {a : Array Nat} (h : Marks n stamp a fun (x : Nat) => x ∈ old) : Diff n stamp old [] a n

theorem Hex.GraphIso.Nauty.Sparse.Diff.hit {n stamp : Nat} {old seen : List Nat} {a : Array Nat} {mina v : Nat} (h : Diff n stamp old seen a mina) (hs : 0 < stamp) (hv : v < n) (hmark : a[v]! = stamp) : Diff n stamp old (seen ++ [v]) (a.set! v 0) mina

theorem Hex.GraphIso.Nauty.Sparse.Diff.miss {n stamp : Nat} {old seen : List Nat} {a : Array Nat} {mina v : Nat} (h : Diff n stamp old seen a mina) (hv : v < n) (hn : ¬v ∈ seen) (hmark : a[v]! ≠ stamp) : Diff n stamp old (seen ++ [v]) a (min mina v)

theorem Hex.GraphIso.Nauty.Sparse.Diff.sentinel {n stamp : Nat} {old seen : List Nat} {a : Array Nat} {mina : Nat} (h : Diff n stamp old seen a mina) (hm : mina = n) : seen ⊆ old