structure Hex.GraphIso.Nauty.Sparse.ActiveSpan {n : Nat} (level first last : Nat) (before active : VSet n) (ptn : Array Nat) : Prop

Before largest-fragment replacement, every new interior fragment is active and the original cell start retains its incoming membership.

• outside (u : Nat) : u < first ∨ last ≤ u → active.mem u = before.mem u
• head : active.mem first = before.mem first
• inner (u : Nat) : first < u → u < last → ptn[u - 1]! ≤ level → active.mem u = true

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.insert_outside {n first last : Nat} {active : VSet n} {v : Nat} (hf : first ≤ v) (hl : v < last) (u : Nat) : u < first ∨ last ≤ u → (active.insert v).mem u = active.mem u

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.initial {n level first last : Nat} {active : VSet n} {ptn : Array Nat} (hc : IsCell ptn level first (last - first)) : ActiveSpan level first last active active ptn

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.cut_push {n level first last cut : Nat} {before active : VSet n} {ptn : Array Nat} (h : ActiveSpan level first last before active ptn) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) : ActiveSpan level first last before (active.insert cut) (ptn.setIfInBounds (cut - 1) level)

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.cut_next {n level first last cut : Nat} {before active : VSet n} {ptn : Array Nat} (h : ActiveSpan level first last before active ptn) (hf : first ≤ cut) (hl : cut + 1 < last) (hb : last ≤ n) : ActiveSpan level first last before (active.insert (cut + 1)) (ptn.setIfInBounds cut level)

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.finish {n level first last : Nat} {before active : VSet n} {ptn : Array Nat} (h : ActiveSpan level first last before active ptn) : CellActive level first last before active ptn

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.replace {n level first last : Nat} {before active : VSet n} {ptn : Array Nat} {v : Nat} (h : ActiveSpan level first last before active ptn) (hf : first < v) (hl : v < last) (hb : last ≤ n) (ha : active.mem first = false) : CellActive level first last before ((active.erase v).insert first) ptn ∧ ∀ (u : Nat), u < first ∨ last ≤ u → ((active.erase v).insert first).mem u = before.mem u

Replacing one interior fragment by the first fragment leaves exactly that interior fragment as the sole possible inactive fragment.

structure Hex.GraphIso.Nauty.Sparse.QueueSpan (first last base : Nat) (queue : Array Nat) : Prop

Appended queue entries belong to the cell currently being split. The saved largest-fragment position therefore cannot erase another cell.

• size : base ≤ queue.size
• entries (p : Nat) : base ≤ p → p < queue.size → first < queue[p]! ∧ queue[p]! < last

theorem Hex.GraphIso.Nauty.Sparse.QueueSpan.initial {first last : Nat} (queue : Array Nat) : QueueSpan first last queue.size queue

theorem Hex.GraphIso.Nauty.Sparse.QueueSpan.push {first last base : Nat} {queue : Array Nat} {v : Nat} (h : QueueSpan first last base queue) (hf : first < v) (hl : v < last) : QueueSpan first last base (queue.push v)

theorem Hex.GraphIso.Nauty.Sparse.ActiveSpan.replace_get {n level first last base pos : Nat} {before active : VSet n} {ptn queue : Array Nat} (h : ActiveSpan level first last before active ptn) (hq : QueueSpan first last base queue) (hp : base ≤ pos) (hb : pos < queue.size) (hn : last ≤ n) (ha : active.mem first = false) : CellActive level first last before ((active.erase queue[pos]).insert first) ptn ∧ ∀ (u : Nat), u < first ∨ last ≤ u → ((active.erase queue[pos]).insert first).mem u = before.mem u

Read the saved queue position using the bounds established by the executed append operations.