def Hex.GraphIso.Nauty.Sparse.Pending (n level : Nat) (key : Nat → Nat) (ends : Array Nat) (todo : List Nat) (lab ptn : Array Nat) : Prop

Cells not covered by the remaining touched-cell windows already have constant semantic counts. The windows use the captured original endpoints.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Pending.initial {lab ptn starts ends before marks touched hits : Array Nat} {n stamp level : Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) (hi : Index.Valid n lab ptn level starts ends) : Pending n level (fun (a : Nat) => List.count a seen) ends touched.toList lab ptn

Singleton cells and untouched cells already have constant counts before the touched-cell fold starts.

theorem Hex.GraphIso.Nauty.Sparse.Pending.step {n : Nat} {key : Nat → Nat} {ends : Array Nat} {todo : List Nat} (level first : Nat) (s : RefineSt n) (h : Pending n level key ends (first :: todo) s.lab s.ptn) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hb : s.cellend[first]! < n) (he : s.cellend[first]! = ends[first]!) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (hv : ∀ (v : Nat), v ∈ segN s.lab first (s.cellend[first]! + 1 - first) → s.hits[v]! = key v) : Pending n level key ends todo (splitCounts level first false s).lab (splitCounts level first false s).ptn

Processing the head touched cell establishes constant counts on its fragments and retains the guarantees of every disjoint completed cell.

theorem Hex.GraphIso.Nauty.Sparse.Pending.done {n level : Nat} {key : Nat → Nat} {ends lab ptn : Array Nat} (h : Pending n level key ends [] lab ptn) (a len : Nat) : IsCell ptn level a len → a + len ≤ n → ∀ (q r : Nat), a ≤ q → q < a + len → a ≤ r → r < a + len → key lab[q]! = key lab[r]!

Exhausting the touched-cell list establishes constant counts everywhere.