theorem
Hex.GraphIso.Nauty.Sparse.Compact.extent
{before : Array Nat}
{p : Nat → Bool}
{first upto : Nat}
{seen : List Nat}
{lab hit : Array Nat}
{next : Nat}
(h : Compact before p first upto seen lab hit next)
(hs : seen.length = upto - first)
:
Collected and retained vertices together fill the scanned interval.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.restore
{before : Array Nat}
{p : Nat → Bool}
{first last : Nat}
{seen : List Nat}
{lab hit : Array Nat}
{next : Nat}
{out : Array Nat}
(h : Compact before p first last seen lab hit next)
(hs : seen = List.take (last - first) (List.drop first before.toList))
(hr : Fill lab hit.toList.reverse next hit.toList.reverse.length out)
:
«Sort».Window before out first last
After reverse reinsertion, compaction is a permutation of exactly the original interval. This includes both uniform-predicate cases.