def
Hex.GraphIso.Nauty.Sparse.fuelContract
{n k : Nat}
(G : Sparse.Colored n k)
:
Generic.Contract (State n) n
The production frame contract with conditional absence of exhaustion. The existing level and cursor bounds suffice; truncated calls retain frames.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.fuel_node_reach
{n k : Nat}
{G : Sparse.Colored n k}
{fuel : Nat}
{f : Generic.NodeFn (State n)}
(h : (fuelContract G).nodeValid fuel f)
:
(reachContract G).nodeValid fuel f
theorem
Hex.GraphIso.Nauty.Sparse.fuel_sweep_reach
{n k : Nat}
{G : Sparse.Colored n k}
{fuel cfuel : Nat}
{f : Generic.SweepFn (State n) n}
(h : (fuelContract G).sweepValid fuel cfuel f)
:
(reachContract G).sweepValid fuel cfuel f
theorem
Hex.GraphIso.Nauty.Sparse.fuel_node
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel : Nat)
{fuel : Nat}
{next : Generic.SweepFn (State n) n}
(hnext : (fuelContract G).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(h : NodeInv G level numcells st)
(hf : n + 1 ≤ level + (fuel + 1))
:
(Generic.nodeStep (Graph.ofGraph G.graph) tcLevel next first level numcells st).fst ≠ Generic.Exit.fuel
Local refinement and classification cannot exhaust the remaining node budget. Every recursive sweep receives a valid equitable parent and cursor.