def Hex.GraphIso.Nauty.Sparse.Max.Parent.back {n : Nat} (G : SparseGraph n) (tcLevel fuel : Nat) (p : Parent n) : State n

The literal state after an off-path child, fixed-point cleanup and native parent recovery. Both filters change only the target vertex set.

Equations

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

structure Hex.GraphIso.Nauty.Sparse.Max.Resumed {n k : Nat} (G : Sparse.Colored n k) (tcLevel : Nat) (p : Parent n) (ds fs : List Nat) (out : State n) (parents : Parents n) : Prop

The native comparisons, histories and ancestor facts available to the next sibling after receiving an off-path child.

• machine : Comparison G.graph (Parent.child G.graph tcLevel p).codes ds fs out
• codes : CodeReady G tcLevel p.node.level (Frame.target G.graph tcLevel p.node).numcells out
• recorded : CheapRecorded p.node.level p.tc out
• route : RouteRecorded G.graph tcLevel p.node.level p.tc out
• scope : Scope G tcLevel p.node ds out parents
• grows : Grows (State.key G.graph p.bs p.state) (State.key G.graph ds out)
• next (cell : VSet n) : (∀ (v : Nat), cell.mem v = true → p.cell.mem v = true) → ∀ (tv : Nat), cell.mem tv = true → Parent.Valid G tcLevel (p.next out ds cell tv)

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.receive {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {p : Parent n} {fs : List Nat} {parents : Parents n} (h : Scope G tcLevel p.node p.bs p.state parents) (hp : Parent.Valid G tcLevel p) (hi : CodeReady G tcLevel p.node.level (Frame.target G.graph tcLevel p.node).numcells p.state) (hc : Comparison G.graph (Parent.child G.graph tcLevel p).codes p.bs fs p.state) (hrecord : CheapRecorded p.node.level p.tc p.state) (hroute : RouteRecorded G.graph tcLevel p.node.level p.tc p.state) (hf : n ≤ p.node.level + fuel) : have ch := Parent.child G.graph tcLevel p; have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd; ∃ (ds : List Nat), ReturnCodes G.graph ch.codes ds fs out ∧ Resumed G tcLevel p ds fs (Parent.back G.graph tcLevel fuel p) parents

A complete actual child supplies the next sibling's entire native context. The ancestor, choice and cheap-shape facts are derived from the executed call and recovery, without assuming its maximum theorem.