def
Hex.GraphIso.Nauty.Sparse.fixedContract
{n k : Nat}
(G : Sparse.Colored n k)
:
Generic.Contract (State n) n
Every call restores its incoming fixed-point set. Entry singletons make each temporary child vertex fresh; recovered parents remain equitable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.fixed_node
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel : Nat)
{fuel : Nat}
{next : Generic.SweepFn (State n) n}
(hnext : (fixedContract G).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(h : NodeInv G level numcells st)
(hf : FixedCells level st.frame)
:
(Generic.nodeStep (Graph.ofGraph G.graph) tcLevel next first level numcells st).snd.fixedpts = st.fixedpts
Native node preparation preserves the fixed singletons and their bitset; all exit arms inherit exact restoration from the child sweep.