theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.congr
{n k : Nat}
{G : Sparse.Colored n k}
{base level : Nat}
{st out next : State n}
(h : FrameOut G base level st out)
(hl : next.lab = out.lab)
(hp : next.ptn = out.ptn)
(hf : next.firstlab = out.firstlab)
(hc : next.canonlab = out.canonlab)
(hs : Scratch.Bounded n next.canong.scratch)
:
FrameOut G base level st next
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.afterChild
{n k : Nat}
{G : Sparse.Colored n k}
{base level : Nat}
{st out : State n}
(h : FrameOut G base level st out)
(depth tv : Nat)
:
FrameOut G base level st (afterChildFirst depth tv out)
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.leave
{n k : Nat}
{G : Sparse.Colored n k}
{base level : Nat}
{st out : State n}
(h : FrameOut G base level st out)
(tv : Nat)
:
FrameOut G base level st
{ 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 }
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.afterSweep
{n k : Nat}
{G : Sparse.Colored n k}
{base level : Nat}
{st out : State n}
(h : FrameOut G base level st out)
(first : Bool)
(depth size index : Nat)
:
FrameOut G base level st (Generic.Policy.afterSweep first depth size index out)
theorem
Hex.GraphIso.Nauty.Sparse.NodeInv.initial
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
:
have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val;
NodeInv G 1 p.snd.length (Sparse.initial (Graph.ofGraph G.graph) p.fst p.snd)
Stable colour buckets establish all production entry assertions.