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

The ordinary native frame contract together with preservation of any fixed suspended ancestor. The latter implication is proved by the policy induction; it is not an assumption about a completed production call.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.traceFrame_node {n k : Nat} (G : Sparse.Colored n k) {base cells : Nat} {root : State n} (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) (tcLevel : Nat) {fuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (traceFrameContract G base root).sweepValid fuel (n + 1) next) (first : Bool) (level numcells : Nat) (st : State n) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) (hlevel : base < level) (h : TraceFrame G base root st) : TraceFrame G base root (Generic.nodeStep (Graph.ofGraph G.graph) tcLevel next first level numcells st).snd

Actual node preparation, either terminal action, and the returned sweep preserve the frozen reference and generator frame.