def Hex.GraphIso.Nauty.Sparse.Max.NodeUpper {n k : Nat} (G : Sparse.Colored n k) (tcLevel fuel : Nat) : Prop

The upper-bound contract of the actual native off-path node at a fixed recursion bound. Its smaller instance is the node induction premise.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.upper_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel : Nat) (hd : NodeUpper G tcLevel fuel) (cfuel : Nat) (first : Bool) (f : Frame n) (bs fs : List Nat) (tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (parents : Parents n) (hvalid : Frame.Valid G f) (h : CodeReady G tcLevel f.level (Frame.target G.graph tcLevel f).numcells st) (hparents : ∀ (tv : Nat), cell.mem tv = true → Parent.Valid G tcLevel { node := f, first := first, state := st, tc := tc, cell := cell, chosen := tv, bs := bs }) (hs : Scope G tcLevel f bs st parents) (hv : ∀ (v : Nat), cursor = some v → cell.mem v = true) (hpast : Generic.Past first tv1 cursor) (hrecord : CheapRecorded f.level tc st) (hroute : RouteRecorded G.graph tcLevel f.level tc st) (hfuel : n ≤ f.level + fuel) (hcursor : Generic.CursorFuel n cfuel cursor) (hc : Comparison G.graph (f.codes ++ [Frame.code G.graph f]) bs fs st) (hphase : st.compCanon ≤ 0 ∨ first = false ∧ cursor.isSome = true) : Bounded (Frame.key G.graph tcLevel f) (State.key G.graph bs st) (State.best G.graph (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel f.level (Frame.target G.graph tcLevel f).numcells tc tv1 cursor cell index st).snd.snd)

The actual native sibling recursion preserves the frozen node's upper bound. Both filters, skipped vertices, nonlocal exits and recovered hinted targets are covered; only the smaller node contract is assumed.