def Hex.GraphIso.Nauty.Sparse.Join.marked (keys seen : List Nat) (p : Nat → Bool) : Nat

Count qualifying cells that have already occurred in a neighbour scan.

Equations

• Hex.GraphIso.Nauty.Sparse.Join.marked keys seen p = List.countP (fun (k : Nat) => decide (k ∈ seen) && p k) keys

theorem Hex.GraphIso.Nauty.Sparse.Join.marked_congr {keys seen seen' : List Nat} {p : Nat → Bool} (h : ∀ (k : Nat), k ∈ keys → (k ∈ seen ↔ k ∈ seen')) : marked keys seen p = marked keys seen' p

theorem Hex.GraphIso.Nauty.Sparse.Join.marked_absent {keys seen : List Nat} {k : Nat} {p : Nat → Bool} (h : ¬k ∈ keys) : marked keys (seen ++ [k]) p = marked keys seen p

theorem Hex.GraphIso.Nauty.Sparse.Join.marked_add {keys seen : List Nat} {k : Nat} {p : Nat → Bool} (hn : keys.Nodup) (hk : k ∈ keys) : marked keys (seen ++ [k]) p = marked keys seen p + if k ∈ seen then 0 else if p k = true then 1 else 0

Clearing a cell after its first occurrence counts it exactly once.

structure Hex.GraphIso.Nauty.Sparse.Join.Counts (keys seen : List Nat) (hits : Array Nat) : Prop

Hit counts after the first edge pass, on the keys the pass can touch.

• bound (k : Nat) : k ∈ keys → k < hits.size
• get (k : Nat) : k ∈ keys → hits[k]! = List.count k seen

theorem Hex.GraphIso.Nauty.Sparse.Join.Counts.initial {keys : List Nat} {hits : Array Nat} (hb : ∀ (k : Nat), k ∈ keys → k < hits.size) (hz : ∀ (k : Nat), k ∈ keys → hits[k]! = 0) : Counts keys [] hits

theorem Hex.GraphIso.Nauty.Sparse.Join.Counts.add {keys seen : List Nat} {hits : Array Nat} {k : Nat} (h : Counts keys seen hits) (hk : k ∈ keys) : Counts keys (seen ++ [k]) (hits.set! k (hits[k]! + 1))

theorem Hex.GraphIso.Nauty.Sparse.Join.Counts.skip {keys seen : List Nat} {hits : Array Nat} {k : Nat} (h : Counts keys seen hits) (hk : ¬k ∈ keys) : Counts keys (seen ++ [k]) hits