def Hex.GraphIso.Nauty.Sparse.Limited.Counted {n : Nat} (s : State n) : Prop

The quota counter counts the native search's actual node visits.

Equations

• Hex.GraphIso.Nauty.Sparse.Limited.Counted s = (s.value.numnodes = s.visited)

theorem Hex.GraphIso.Nauty.Sparse.Limited.map_counted {n : Nat} {s : State n} (h : Counted s) (f : Sparse.State n → Sparse.State n) (hf : (f s.value).numnodes = s.value.numnodes) : Counted (map f s)

theorem Hex.GraphIso.Nauty.Sparse.Limited.visit_counted {n : Nat} {s : State n} (h : Counted s) (g : Graph n) (level nc : Nat) : Counted (visit g level nc s).snd.snd

theorem Hex.GraphIso.Nauty.Sparse.Limited.countPolicy {n : Nat} (g : Graph n) (inf tcLevel : Nat) : Generic.Preserve g inf tcLevel Counted

Every native callback preserves the equality of the two counters; only visit increments them, together, after admission.

theorem Hex.GraphIso.Nauty.Sparse.Limited.node_counted {n : Nat} {s : State n} (h : Counted s) (g : Graph n) (inf tcLevel fuel level nc : Nat) (first : Bool) : Counted (Generic.node first g inf tcLevel fuel level nc s).snd

theorem Hex.GraphIso.Nauty.Sparse.Limited.node_nodes {n limit : Nat} {s : State n} (hb : Budget limit s) (hc : Counted s) (g : Graph n) (inf tcLevel fuel level nc : Nat) (first : Bool) : (Generic.node first g inf tcLevel fuel level nc s).snd.value.numnodes ≤ limit

The actual node count is bounded even for an exhausted return.

theorem Hex.GraphIso.Nauty.Sparse.Limited.run?_counted {n limit : Nat} {g : Graph n} {lab : Array Nat} {ends : List Nat} {s : State n} (h : run? limit g lab ends = some s) : Counted s

A completed bounded root reports exactly its admitted native visits.

theorem Hex.GraphIso.Nauty.Sparse.Limited.run?_nodes {n limit : Nat} {g : Graph n} {lab : Array Nat} {ends : List Nat} {s : State n} (h : run? limit g lab ends = some s) : s.value.numnodes ≤ limit

theorem Hex.GraphIso.Nauty.Sparse.Limited.runColored?_nodes {n k limit : Nat} {G : Sparse.Colored n k} {s : State n} (h : runColored? limit G = some s) : s.value.numnodes ≤ limit

theorem Hex.GraphIso.Nauty.Sparse.Limited.runPair?_nodes {n k limit : Nat} {G H : Sparse.Colored n k} {a b : State n} (h : runPair? limit G H = some (a, b)) : a.value.numnodes + b.value.numnodes ≤ limit

The two native traversals together fit the single supplied quota.