structure
Hex.GraphIso.Nauty.Sparse.RefineSt.Ready
{n : Nat}
(G : SparseGraph n)
(level : Nat)
(s : RefineSt n)
:
A post-refinement native node. The certificate records the actual active set; equitability justifies the next individualization.
- equitable : Equitable (Graph.context G) level s.lab s.ptn
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.SpecNode.refineWith
{n : Nat}
{G : SparseGraph n}
{level numcells : Nat}
{lab ptn : Array Nat}
{active : VSet n}
(h : SpecNode G level lab ptn active numcells)
(scratch : Scratch)
(hb : Scratch.Bounded n scratch)
:
RefineSt.Ready G level (Sparse.refineWith (Graph.ofGraph G) level lab ptn active numcells scratch)
Tree-entry invariants hold for the actual cached refinement as well as fresh refinement. Incoming scratch may have any proved bounded contents.
def
Hex.GraphIso.Nauty.Sparse.RefineSt.child
{n : Nat}
(g : Graph n)
(level : Nat)
(s : RefineSt n)
(tc tv : Nat)
(scratch : Scratch)
:
RefineSt n
The exact individualization and cached refinement performed by a native child call; the supplied scratch is the call's actual storage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.child
{n : Nat}
{G : SparseGraph n}
{level : Nat}
{s : RefineSt n}
(h : Ready G level s)
{tc len o : Nat}
(hc : IsCell s.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ho : o < len)
(scratch : Scratch)
(hs : Scratch.Bounded n scratch)
:
Ready G (level + 1) (RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + o]! scratch)
Every member of a nontrivial cell gives a valid equitable child under the literal native child operation, independently of bounded scratch.