theorem
Hex.GraphIso.Nauty.Sparse.NodeInv.prepare_frame
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : NodeInv G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(tcLevel : Nat)
:
FrameOut G (level - 1) level st (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd.snd
Actual first preparation has the native node frame effect before any child or terminal action occurs.
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.first_seed
{n k : Nat}
{G : Sparse.Colored n k}
{base cells level numcells : Nat}
{root st : State n}
(h : FrameOut G base base root st)
(hp : Ready G base cells root)
(hr : Ready G level numcells st)
(hn : 0 < n)
(hb : 1 ≤ base)
(hlevel : base ≤ level)
(ht : st.genTrace = #[])
(hw : st.workperm.size = n)
:
TraceFrame G base root (firstterminal level st)
The first terminal action seeds both reference frames from the actual leaf label and the empty incoming trace. No reference containment is assumed before the first leaf has been installed.