def Hex.GraphIso.Nauty.Sparse.State.refined {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : RefineSt n

The literal cached refinement performed by a production node.

Equations

• Hex.GraphIso.Nauty.Sparse.State.refined g level numcells st = Hex.GraphIso.Nauty.Sparse.refineWith g level st.lab st.ptn st.active numcells st.canong.scratch

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.refined {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) : RefineSt.Ready G.graph level (State.refined (Graph.ofGraph G.graph) level numcells st)

theorem Hex.GraphIso.Nauty.Sparse.prepareFirst_partition {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : have r := Generic.prepareFirst g tcLevel level numcells st; r.snd.snd.snd.snd.lab = (State.refined g level numcells st).lab ∧ r.snd.snd.snd.snd.ptn = (State.refined g level numcells st).ptn ∧ r.fst = (State.refined g level numcells st).numcells

First preparation retains exactly the partition and count returned by its cached visit while recording the reference code and target.

theorem Hex.GraphIso.Nauty.Sparse.firstChild_refined {n : Nat} (g : Graph n) (tcLevel level numcells tv : Nat) (st : State n) : have r := Generic.prepareFirst g tcLevel level numcells st; have child := Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd); State.refined g (level + 1) (r.fst + 1) child = RefineSt.child g level (State.refined g level numcells st) r.snd.fst.toNat tv child.canong.scratch

The first child's production visit is a step of the native descent relation with precisely the scratch stored by that child transition.