def Hex.GraphIso.Nauty.Generation.Counted (vertices : List Nat) (P : Nat → Prop) (cursor : Option Nat) (index : Nat) : Prop

A sweep counter counts distinct original vertices already known to satisfy a property. Witnesses lie behind the cursor, so advancing it can never count the same vertex twice. The mutable target set may shrink.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Generation.Counted.start (vertices : List Nat) (P : Nat → Prop) : Counted vertices P none 0

The first-path orbit counter starts with no marked vertices.

theorem Hex.GraphIso.Nauty.Generation.Counted.advance {vertices : List Nat} {P : Nat → Prop} {cursor : Option Nat} {index : Nat} (h : Counted vertices P cursor index) {tv : Nat} {mark : Bool} (ha : After cursor tv) (hm : tv ∈ vertices) (hp : mark = true → P tv) : Counted vertices P (some tv) (if mark = true then index + 1 else index)

A counter increment records precisely the current vertex; a failed mark only advances the cursor. This is the update used by firstChildLoop.

theorem Hex.GraphIso.Nauty.Generation.Counted.mono {vertices : List Nat} {P Q : Nat → Prop} {cursor : Option Nat} {index : Nat} (h : Counted vertices P cursor index) (hp : ∀ (v : Nat), P v → Q v) : Counted vertices Q cursor index

Previously counted properties may be transported along an implication, for example by retaining their generator words in a later trace.

theorem Hex.GraphIso.Nauty.Generation.Counted.full {vertices : List Nat} {P : Nat → Prop} {cursor : Option Nat} {index : Nat} (h : Counted vertices P cursor index) (hfull : vertices.length ≤ index) (v : Nat) : v ∈ vertices → P v

A counter equal to the original target size certifies the property for every original vertex. No assertion about the surviving target set is needed.

theorem Hex.GraphIso.Nauty.Generation.Counted.cellStep {vertices : List Nat} {cursor : Option Nat} {index n level guide tv : Nat} {g : Array (VSet n)} {ptn lab orbits : Array Nat} {store : List (Array Nat)} (h : Counted vertices (fun (v : Nat) => ∃ (γ : Array Nat), checkAutom g γ = true ∧ CellStab ptn level lab γ ∧ γ[v]! = guide) cursor index) (ha : After cursor tv) (hm : tv ∈ vertices) (htv : tv < n) (hok : LabOk lab n) (hsp : ptn.size = n) (hs : lab.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hsound : OrbSound (OrbConn store n) orbits n) (hcheck : ∀ (γ : Array Nat), γ ∈ store → checkAutom g γ = true) (hstab : ∀ (γ : Array Nat), γ ∈ store → CellStab ptn level lab γ) : Counted vertices (fun (v : Nat) => ∃ (γ : Array Nat), checkAutom g γ = true ∧ CellStab ptn level lab γ ∧ γ[v]! = guide) (some tv) (if (orbits[tv]! == guide) = true then index + 1 else index)

The orbit-counter test also retains a checked carrier in the frozen cell stabilizer, without requiring a root trace inclusion premise.