theorem
Hex.GraphIso.Nauty.SearchOk.iter
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells : Nat}
{st : Search n}
{r : RefineSt n}
(h : SearchOk G level numcells st)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hl : r.lab = st.lab)
(hp : r.ptn = st.ptn)
:
IterOk ctx level r
A reached search partition supplies the geometric descent invariant for any refinement state with those same partition arrays.
theorem
Hex.GraphIso.Nauty.SearchOk.subtree
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells : Nat}
{st : Search n}
{r : RefineSt n}
(h : SearchOk G level numcells st)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hl : r.lab = st.lab)
(hp : r.ptn = st.ptn)
(hc : r.numcells = numcells)
(he : Equitable ctx level st.lab st.ptn)
(hs : NodeShape n level st.ptn)
:
SubtreeOk ctx level r
Small-cell shape together with the existing reach, count, and equitability facts gives the complete subtree invariant.