def
Hex.GraphIso.Nauty.GuidedAt
{n : Nat}
(ctx : Ctx n)
(tcLevel : Nat)
(store : Array Int)
(base : Nat)
(root : RefineSt n)
(level numcells : Nat)
(st : Search n)
:
A guided history ending at 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.GuidedAt.congr
{n : Nat}
{ctx : Ctx n}
{store : Array Int}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st out : Search n}
(h : GuidedAt ctx tcLevel store base root level numcells st)
(hl : out.lab = st.lab)
(hp : out.ptn = st.ptn)
:
GuidedAt ctx tcLevel store base root level numcells out
Changes to other fields leave the guided endpoint unchanged.
theorem
Hex.GraphIso.Nauty.GuidedAt.recover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{store : Array Int}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st out : Search n}
(h : GuidedAt ctx tcLevel store base root level numcells st)
(hok : SearchOk G level numcells st)
(hout : SearchOut G level level st out)
:
GuidedAt ctx tcLevel store base root level numcells (Nauty.recover (n + 2) level out)
Restoring a parent after a child preserves the parent's guided history.
theorem
Hex.GraphIso.Nauty.GuidedAt.child
{n : Nat}
{ctx : Ctx n}
{store : Array Int}
{tcLevel base level numcells tc e o : Nat}
{root : RefineSt n}
{st : Search n}
(h : GuidedAt ctx tcLevel 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 : specTargetcell ctx st.lab st.ptn level tcLevel = tc ∨ store[level]! = Int.ofNat tc)
:
GuidedPerm ctx tcLevel store base root (level + 1)
(SearchState.refined ctx (level + 1) (numcells + 1) (Nauty.child false level tc st.lab[tc + o]! st))
A canonical or saved target extends the executable guided descent.
theorem
Hex.GraphIso.Nauty.GuidedAt.equitable
{n : Nat}
{ctx : Ctx n}
{store : Array Int}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st : Search n}
(h : GuidedAt ctx tcLevel store base root level numcells st)
(hok : IterOk ctx base root)
(heq : Equitable ctx base root.lab root.ptn)
(hacc : bcount root.ptn base n = root.numcells)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
:
Equitability of the guided history gives equitability of the current partition.