theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_cover {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {cs : List Nat} {st : State n} {best : Option (Key n)} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hf : n < fuel + 1 + numcells) : have r := visit (Graph.ofGraph G.graph) level numcells st; have t := maketargetCached (Graph.ofGraph G.graph) r.snd.snd.lab r.snd.snd.ptn level tcLevel (-1) r.snd.snd.canong.scratch; r.fst < n → (Covers (prefixKey cs (subtreeKey G.graph tcLevel (fuel + 1) level st.lab st.ptn st.active numcells)) best ↔ ∀ (v : Nat), t.snd.fst.mem v = true → Covers (prefixKey (cs ++ [r.snd.fst]) (vertexKey G.graph tcLevel fuel level r.snd.snd.lab r.snd.snd.ptn t.fst r.fst v)) best)

Full coverage of an internal node is exactly coverage of all children of its actual cached target, including the frozen ancestor code prefix.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_finish {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {cs : List Nat} {st : State n} {best : Option (Key n)} {live : Nat → Prop} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hf : n < fuel + 1 + numcells) : have r := visit (Graph.ofGraph G.graph) level numcells st; have t := maketargetCached (Graph.ofGraph G.graph) r.snd.snd.lab r.snd.snd.ptn level tcLevel (-1) r.snd.snd.canong.scratch; r.fst < n → CellCover G.graph tcLevel fuel level r.fst t.fst t.snd.snd.fst (cs ++ [r.snd.fst]) r.snd.snd live best → (∀ (v : Nat), ¬live v) → Covers (prefixKey cs (subtreeKey G.graph tcLevel (fuel + 1) level st.lab st.ptn st.active numcells)) best

Exhausting the live representatives of an actual cached target covers the original complete node. Earlier filter removals are accounted for by the ranked child-coverage invariant.