def
Hex.GraphIso.Nauty.DescentAt
{n : Nat}
(ctx : Ctx n)
(store : Array Int)
(base : Nat)
(root : RefineSt n)
(level numcells : Nat)
(st : Search n)
:
A mathematical descent agrees with the executable partition and cell count.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.DescentAt.congr
{n : Nat}
{ctx : Ctx n}
{store : Array Int}
{base level numcells : Nat}
{root : RefineSt n}
{st out : Search n}
(h : DescentAt ctx store base root level numcells st)
(hlab : out.lab = st.lab)
(hptn : out.ptn = st.ptn)
:
DescentAt ctx store base root level numcells out
Bookkeeping that preserves the partition preserves its descent history.
theorem
Hex.GraphIso.Nauty.DescentAt.recover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{store : Array Int}
{base level numcells : Nat}
{root : RefineSt n}
{st out : Search n}
(h : DescentAt ctx store base root level numcells st)
(hok : SearchOk G level numcells st)
(hout : SearchOut G level level st out)
:
DescentAt ctx store base root level numcells (Nauty.recover (n + 2) level out)
Recovering a completed child retains the parent's history up to label order within its cells, even though the child's labelling is kept.
theorem
Hex.GraphIso.Nauty.DescentAt.child
{n : Nat}
{ctx : Ctx n}
{store : Array Int}
{base level numcells tc e o : Nat}
{root : RefineSt n}
{st : Search n}
(h : DescentAt ctx store base root level numcells st)
(hsize : ctx.g.size = n)
(hroot : IterOk ctx base root)
(hlevel : level < n)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(ho : o ≤ e - tc)
(htc : store[level]! = Int.ofNat tc)
:
FollowsPerm ctx store base root (level + 1)
(SearchState.refined ctx (level + 1) (numcells + 1) (Nauty.child false level tc st.lab[tc + o]! st))
Individualizing a vertex in the recorded target and refining it extends the executable descent history.
theorem
Hex.GraphIso.Nauty.DescentAt.target
{n : Nat}
{ctx : Ctx n}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st : Search n}
(h : DescentAt ctx st.firsttc base root level numcells st)
(href : FirstRef ctx tcLevel base root st)
(hdepth : Depth href.last st)
(heq : st.eqlevFirst = level)
(hkeep : (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd.eqlevFirst = level)
(hnc : numcells < n)
(hlevel : 0 < level)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hsmall : SubtreeOk ctx base root)
:
At a cheap ancestor, retaining code agreement forces the executable target choice to extend the saved descent history.