def Hex.GraphIso.Nauty.Sparse.CellCover {n : Nat} (G : SparseGraph n) (tcLevel fuel level numcells tc len : Nat) (cs : List Nat) (st : State n) (live : Nat → Prop) (best : Option (Key n)) : Prop

Coverage of a frozen target cell, indexed by vertex labels. Live vertices can include the cursor condition as well as mutable set membership.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.CellCover.init {n : Nat} (G : SparseGraph n) (tcLevel fuel level numcells tc len : Nat) (cs : List Nat) (st : State n) (best : Option (Key n)) : CellCover G tcLevel fuel level numcells tc len cs st (fun (v : Nat) => (windowSet n st.lab tc len).mem v = true) best

Before visiting children, every target vertex represents itself.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.grow {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st : State n} {live : Nat → Prop} {before after : Option (Key n)} (h : CellCover G tcLevel fuel level numcells tc len cs st live before) (hg : Grows before after) : CellCover G tcLevel fuel level numcells tc len cs st live after

Growing the incumbent preserves all previously covered children.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.visit {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells tc len tv : Nat} {cs : List Nat} {st : State n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover G tcLevel fuel level numcells tc len cs st live best) (hle : ∀ (v : Nat), live v → tv ≤ v) (hc : Covers (prefixKey cs (vertexKey G tcLevel fuel level st.lab st.ptn tc numcells tv)) best) : CellCover G tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ tv < v) best

Visiting the least live vertex advances the cursor and absorbs every original child represented by that vertex.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.skip {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells tc len tv rep : Nat} {cs : List Nat} {st : State n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover G tcLevel fuel level numcells tc len cs st live best) (hle : ∀ (v : Nat), live v → tv ≤ v) (hr : (windowSet n st.lab tc len).mem rep = true) (hlt : rep < tv) (hkey : vertexKey G tcLevel fuel level st.lab st.ptn tc numcells tv = vertexKey G tcLevel fuel level st.lab st.ptn tc numcells rep) : CellCover G tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ tv < v) best

A child repeating a smaller representative is already covered when it reaches the cursor. Ranked coverage rules out a still-live carrier below that cursor, including after earlier filters.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.finish {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st : State n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover G tcLevel fuel level numcells tc len cs st live best) (hempty : ∀ (v : Nat), ¬live v) (v : Nat) : (windowSet n st.lab tc len).mem v = true → Covers (prefixKey cs (vertexKey G tcLevel fuel level st.lab st.ptn tc numcells v)) best

Exhausting the live set covers the full original target cell.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.finish_cursor {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st : State n} {live : Nat → Prop} {best : Option (Key n)} {cell : VSet n} {cursor : Option Nat} (h : CellCover G tcLevel fuel level numcells tc len cs st live best) (hmem : ∀ (v : Nat), live v → cell.mem v = true) (hle : ∀ (v : Nat), live v → VSet.scanStart cursor ≤ v) (hnone : cell.nextElem cursor = none) (v : Nat) : (windowSet n st.lab tc len).mem v = true → Covers (prefixKey cs (vertexKey G tcLevel fuel level st.lab st.ptn tc numcells v)) best

The executable cursor terminator exhausts every live member at or after its scan start, closing coverage of the original target cell.