theorem
Hex.GraphIso.Nauty.Sparse.Binary.Cell.preserve
{level first last : Nat}
{pred : Nat → Bool}
{n✝ : Nat}
{s t : RefineSt n✝}
{a len : Nat}
(h : Cell level first last pred s t)
(hc : IsCell s.ptn level first (last - first))
(ha : IsCell s.ptn level a len)
(hne : a ≠ first)
:
Processing one cell preserves every other cell's partition boundaries.
theorem
Hex.GraphIso.Nauty.Sparse.Binary.Cell.valid
{n level first last : Nat}
{pred : Nat → Bool}
{s t : RefineSt n}
(h : Cell level first last pred s t)
(hp : s.lab.toList.Perm (List.range n))
(hs : s.ptn.size = n)
(hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend)
(hc : IsCell s.ptn level first (last - first))
(hn : first + 1 < last)
:
The next cell receives a labelling permutation, allocated partition and valid cache from the preceding executed cell body.