def
Hex.GraphIso.Nauty.Sparse.Max.Parent.firstBack
{n : Nat}
(G : SparseGraph n)
(tcLevel fuel : Nat)
(p : Parent n)
:
State n
The literal first-child return, including its first-ancestor update, fixed-point cleanup and native parent recovery.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.receive
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel tv last : Nat}
{f : Frame n}
{leaf : State n}
{parents : Parents n}
(h : FirstEntry G f)
(hs : Scope G tcLevel f [] f.entry parents)
(hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n)
(htv :
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true f.level
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells
f.entry).snd.snd.snd.snd).orbits[tv]! = tv)
(path :
have p := Frame.firstParent G.graph tcLevel f [] tv;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (Parent.child G.graph tcLevel p).level
(Parent.child G.graph tcLevel p).numcells (Parent.child G.graph tcLevel p).entry last leaf)
(hf : n ≤ f.level + fuel)
:
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
have out := (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd;
∃ (bs : List Nat), ∃ (fs : List Nat), ReturnCodes G.graph ch.codes bs fs out ∧ Resumed G tcLevel p bs fs (Parent.firstBack G.graph tcLevel fuel p) parents
The executed first child supplies every comparison, history and ancestor fact needed by the later sibling loop. No code or maximum contract for that child is assumed.