theorem
Hex.GraphIso.Nauty.Sparse.filter_transport
{seen visits : List Nat}
(f : Nat → Nat)
(p q : Nat → Bool)
(hp : visits.Perm (List.map f seen))
(hk : ∀ (v : Nat), v ∈ seen → q (f v) = p v)
:
(List.filter q visits).Perm (List.map f (List.filter p seen))
Predicate classes transport through a mapped permutation. Predicate agreement is needed only on the traversed source vertices.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.counts_map
{before : Array Nat}
{p : Nat → Bool}
{first last : Nat}
{seen : List Nat}
{lab hit : Array Nat}
{cut : Nat}
{other : Array Nat}
{q : Nat → Bool}
{visits : List Nat}
{out collected : Array Nat}
{next : Nat}
(f : Nat → Nat)
(hs : Compact before p first last seen lab hit cut)
(ht : Compact other q first last visits out collected next)
(hp : visits.Perm (List.map f seen))
(hk : ∀ (v : Nat), v ∈ seen → q (f v) = p v)
:
The executed compaction's cut and collected-hit count depend only on the transported predicate classes, including either uniform case.