def
Hex.GraphIso.Nauty.Sparse.reachContract
{n k : Nat}
(G : Sparse.Colored n k)
:
Generic.Contract (State n) n
Actual sparse call invariants and frame effects, including arbitrary truncation and nonlocal exits. Parent equitability is restored between siblings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.reach_node
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel : Nat)
{fuel : Nat}
{next : Generic.SweepFn (State n) n}
(hnext : (reachContract G).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(h : NodeInv G level numcells st)
:
FrameOut G (level - 1) level st (Generic.nodeStep (Graph.ofGraph G.graph) tcLevel next first level numcells st).snd
The production node's local work preserves its caller frame when its child sweep does. Refinement establishes all target and equitability premises.