theorem
Hex.GraphIso.Nauty.Sparse.Replay.head_codes
{n : Nat}
{G : SparseGraph n}
{tcLevel fuel level numcells : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{l : SpecLeaf n}
(h : l ∈ specLeaves G tcLevel (fuel + 1) level lab ptn active numcells)
:
Every enumerated leaf starts with the code of the actual refinement. No well-formedness or nonemptiness premise is needed for this local rule.
theorem
Hex.GraphIso.Nauty.Sparse.Replay.code_cmp
{n : Nat}
{G H : SparseGraph n}
{l : SpecLeaf n}
{c b : Nat}
{cs bs : List Nat}
(hc : l.codes = c :: cs)
(hlt : compare c b = Ordering.lt)
:
theorem
Hex.GraphIso.Nauty.Sparse.Replay.prune_valid
{n : Nat}
{G H : SparseGraph n}
{tcLevel fuel level numcells b : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{bs : List Nat}
(h : compare (refine (Graph.ofGraph G) level lab ptn active numcells).longcode b = Ordering.lt)
:
A strictly smaller recomputed code covers the complete native subtree and cannot hide an attaining leaf.