def Hex.GraphIso.Nauty.Sparse.storeContract {n k : Nat} (G : Sparse.Colored n k) : Generic.Contract (State n) n

Every well-formed call preserves its partition frame and any installed native canonical store. The implication permits the independent first-descent argument to seed that store at the actual first leaf.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.store_node_reach {n k : Nat} {G : Sparse.Colored n k} {fuel : Nat} {descend : Generic.NodeFn (State n)} (h : (storeContract G).nodeValid fuel descend) : (reachContract G).nodeValid fuel descend

theorem Hex.GraphIso.Nauty.Sparse.store_sweep_reach {n k : Nat} {G : Sparse.Colored n k} {fuel cfuel : Nat} {next : Generic.SweepFn (State n) n} (h : (storeContract G).sweepValid fuel cfuel next) : (reachContract G).sweepValid fuel cfuel next

theorem Hex.GraphIso.Nauty.Sparse.Ready.parse {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) : ∃ (l : Label n), Label.ofArray? n st.lab = some l

theorem Hex.GraphIso.Nauty.Sparse.store_node {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel : Nat) {fuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (storeContract G).sweepValid fuel (n + 1) next) (first : Bool) (level numcells : Nat) (st : State n) (hl : 1 ≤ level) (h : NodeInv G level numcells st) (hs : Store G.graph st) : Store G.graph (Generic.nodeStep (Graph.ofGraph G.graph) tcLevel next first level numcells st).snd

Actual node preparation, classification and leaf installation preserve the native canonical prefix, before passing it to the child continuation.