theorem
Hex.GraphIso.Nauty.Max.SweepInput.done_cover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{level numcells tc tv1 index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 none cell index st l bs fs parents)
:
Generic.Covers (Loop.bound ctx tcLevel l) (SearchState.key ctx bs st)
An exhausted cursor leaves every vertex of the original target window covered, and hence covers its entire frozen maximum.
theorem
Hex.GraphIso.Nauty.Max.finish
{n k : Nat}
(G : Colored n k)
(tcLevel fuel cfuel : Nat)
(first : Bool)
(level numcells tc tv1 : Nat)
(cell : VSet n)
(index : Nat)
(st : Search n)
:
(keyContract G tcLevel).sweepPost fuel cfuel first level numcells tc tv1 none cell index st
(Generic.Exit.done, index, st)
An exhausted sweep reads the settled incumbent and closes the coverage contract without changing any search state.