def
Hex.GraphIso.Nauty.RouteHistory
{n : Nat}
(ctx : Ctx n)
(tcLevel level agreed numcells : Nat)
(st : Search n)
:
Retain the first descent and the current guided descent at their common ancestor, including outside the cheap-automorphism region.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.RouteHistory.transport
{n : Nat}
{ctx : Ctx n}
{tcLevel level agreed numcells level' agreed' numcells' : Nat}
{st out : Search n}
(h : RouteHistory ctx tcLevel level agreed numcells st)
(hr : SearchState.reference out = SearchState.reference st)
(hg : out.gcaFirst = st.gcaFirst)
(ha :
∀ (root : RefineSt n),
GuidedState ctx tcLevel st.gcaFirst root level agreed numcells st →
GuidedState ctx tcLevel st.gcaFirst root level' agreed' numcells' out)
:
RouteHistory ctx tcLevel level' agreed' numcells' out
Operations preserving the reference and common ancestor transport the guided current descent through their local field changes.
theorem
Hex.GraphIso.Nauty.RouteHistory.compare
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells code : Nat}
{st : Search n}
(h : RouteHistory ctx tcLevel level (level - 1) numcells st)
(hlevel : 0 < level)
:
RouteHistory ctx tcLevel level level numcells (compareCodes level code st)
Comparing a node activates its pending guided history.
theorem
Hex.GraphIso.Nauty.RouteHistory.target
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : RouteHistory ctx tcLevel level level numcells st)
:
RouteHistory ctx tcLevel level level numcells (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd
Selecting a target retains every live guided history.
theorem
Hex.GraphIso.Nauty.RouteHistory.classify
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : RouteHistory ctx tcLevel level level numcells st)
:
RouteHistory ctx tcLevel level level numcells (Nauty.classify ctx level numcells st).snd
Classification retains the guided current partition.
theorem
Hex.GraphIso.Nauty.RouteHistory.leaf
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : RouteHistory ctx tcLevel level level numcells st)
(leaf : Leaf)
:
RouteHistory ctx tcLevel level level numcells (leafExit leaf level st).snd
Leaf actions retain the guided history until an ancestor receives the exit.
theorem
Hex.GraphIso.Nauty.RouteHistory.cheap
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : RouteHistory ctx tcLevel level level numcells st)
(first : Bool)
:
RouteHistory ctx tcLevel level level numcells (cheapCheck first level st)
The cheap guard changes neither the guided history nor its common ancestor.
theorem
Hex.GraphIso.Nauty.RouteHistory.choice
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : RouteHistory ctx tcLevel level level numcells st)
(hnc : numcells < n)
(hlevel : 0 < level)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
:
Retained target agreement satisfies the guided canonical-or-saved rule.
theorem
Hex.GraphIso.Nauty.RouteHistory.child
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells tc tv : Nat}
{st : Search n}
{cell : VSet n}
(h : RouteHistory ctx tcLevel level level numcells st)
(hchoice : Choice ctx tcLevel level tc st)
(first : Bool)
(hsize : ctx.g.size = n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(htv : cell.mem tv = true)
:
have next := Nauty.child first level tc tv st;
have r := visit ctx (level + 1) (numcells + 1) next;
RouteHistory ctx tcLevel (level + 1) level r.fst r.snd.snd
Individualizing a guided target prepares the child's pending route.
theorem
Hex.GraphIso.Nauty.RouteHistory.child_return
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc tv : Nat}
{st : Search n}
{cell : VSet n}
(h : RouteHistory ctx tcLevel level level numcells st)
(first : Bool)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(htv : cell.mem tv = true)
:
have out := (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd;
have result :=
recover (n + 2) level
{ lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv,
autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode,
firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong,
samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon,
gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel,
noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex,
stabvertex := out.stabvertex, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates,
numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves,
maxlevel := out.maxlevel, order := out.order, genTrace := out.genTrace, workperm := out.workperm };
RouteHistory ctx tcLevel level level numcells result ∧ (Choice ctx tcLevel level tc st → Choice ctx tcLevel level tc result)
The actual child return restores its parent's guided history and canonical-or-saved target, using the independent frame and divergence proofs.