theorem
Hex.GraphIso.Nauty.filter_pair
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc len : Nat}
{cell : VSet n}
{st filter : Search n}
{cs : List Nat}
{live : Nat → Prop}
{best : Option (Key n)}
(h : SearchOk G level numcells st)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hgsz : ctx.g.size = n)
(hc : IsCell st.ptn level tc len)
(hr : tc + len ≤ n)
(hfuel : level + 1 + fuel ≤ n + 1)
(hcover : CellCover ctx tcLevel fuel level numcells tc len cs st live best)
(hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true)
(hmem : ∀ (v : Nat), live v → cell.mem v = true)
(hlast : ∀ (fix mcr : VSet n), filter.autos.back? = some (fix, mcr) → PairOk ctx.g st.ptn st.lab level fix mcr)
:
A short filter needs local validity of its newest pair. The pair may come from a returned child's unrecovered state while coverage stays in the parent's partition and labelling.