theorem
Hex.GraphIso.Nauty.firstLeaf_boundary
{n : Nat}
{ctx : Ctx n}
{tcLevel fuel level numcells last bound saved : Nat}
{st leaf : Search n}
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hlevel : bound < level)
(hin : st.noncheaplevel = saved ∨ bound < st.noncheaplevel)
:
The first descent changes its boundary only at a deeper failed guard.
theorem
Hex.GraphIso.Nauty.firstPath_boundary
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hlevel : 0 < level)
:
(node true ctx inf tcLevel fuel level numcells st).snd.noncheaplevel = st.noncheaplevel ∨ level ≤ (node true ctx inf tcLevel fuel level numcells st).snd.noncheaplevel
A full first-path call retains every surviving older boundary.
theorem
Hex.GraphIso.Nauty.Boundary.firstPath
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(h : Boundary G ctx level st)
(hn0 : 0 < n)
(hlevel : 1 < level)
(hok : SearchOk G level numcells st)
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
:
Boundary G ctx level (Nauty.node true ctx (n + 2) tcLevel fuel level numcells st).snd
A first child returns with the implicit pair at every surviving older boundary.