def Hex.GraphIso.Nauty.Generation.Counter {n : Nat} (P : Fin n → Prop) (cursor : Option Nat) (index : Nat) : Prop

The counter is the number of qualifying vertices passed by the actual ascending cursor. The witness records all of them exactly once.

Equations

• Hex.GraphIso.Nauty.Generation.Counter P cursor index = ∃ (seen : List (Fin n)), seen.Nodup ∧ seen.length = index ∧ ∀ (v : Fin n), v ∈ seen ↔ P v ∧ ¬Hex.GraphIso.Nauty.After cursor ↑v

theorem Hex.GraphIso.Nauty.Generation.Counter.start {n : Nat} (P : Fin n → Prop) : Counter P none 0

theorem Hex.GraphIso.Nauty.Generation.Counter.advance {n : Nat} {P : Fin n → Prop} {cursor : Option Nat} {index : Nat} (h : Counter P cursor index) {cell : VSet n} {tv : Fin n} {mark : Bool} (hwindow : ∀ (v : Fin n), P v → cell.mem ↑v = true) (hnext : cell.nextElem cursor = some ↑tv) (hmark : mark = true ↔ P tv) : Counter P (some ↑tv) (if mark = true then index + 1 else index)

Advancing the real target cursor adds precisely its current vertex when the executed mark test agrees with the qualifying property.

theorem Hex.GraphIso.Nauty.Generation.Counter.finish {n : Nat} {P : Fin n → Prop} {cursor : Option Nat} {index : Nat} (h : Counter P cursor index) {cell : VSet n} (hwindow : ∀ (v : Fin n), P v → cell.mem ↑v = true) (hnext : cell.nextElem cursor = none) [DecidablePred P] : index = List.countP (fun (v : Fin n) => decide (P v)) (List.finRange n)

Exhausting the actual target set identifies the accumulated index with the cardinality of the qualifying vertices in the whole graph.