def Hex.GraphIso.Nauty.Orbit.Descending (o : Array Nat) (n : Nat) : Prop

Every parent pointer lies below its vertex.

Equations

• Hex.GraphIso.Nauty.Orbit.Descending o n = (o.size = n ∧ ∀ (v : Nat), v < n → o[v]! ≤ v)

def Hex.GraphIso.Nauty.Orbit.Stable {α : Sort u} (o : Array Nat) (n : Nat) (f : Nat → α) : Prop

A function constant along all parent pointers.

Equations

• Hex.GraphIso.Nauty.Orbit.Stable o n f = ∀ (v : Nat), v < n → f o[v]! = f v

def Hex.GraphIso.Nauty.Orbit.Flat (o : Array Nat) (n : Nat) : Prop

All parent pointers already point to roots.

Equations

• Hex.GraphIso.Nauty.Orbit.Flat o n = ∀ (v : Nat), v < n → o[o[v]!]! = o[v]!

theorem Hex.GraphIso.Nauty.Orbit.Descending.ofSound {n : Nat} {R : Nat → Nat → Prop} {o : Array Nat} (h : OrbSound R o n) : Descending o n

theorem Hex.GraphIso.Nauty.Orbit.Descending.sound {n : Nat} {o : Array Nat} (h : Descending o n) : OrbSound (fun (x x_1 : Nat) => True) o n

theorem Hex.GraphIso.Nauty.Orbit.Descending.set {n : Nat} {o : Array Nat} (h : Descending o n) {p q : Nat} (hq : q < n) (hp : p ≤ q) : Descending (o.set! q p) n

theorem Hex.GraphIso.Nauty.Orbit.Stable.of_set_root {n : Nat} {α : Sort u} {o : Array Nat} {f : Nat → α} {q p : Nat} (hroot : o[q]! = q) (h : Stable (o.set! q p) n f) : Stable o n f

Joining two roots preserves every previous parent equation.

theorem Hex.GraphIso.Nauty.Orbit.Stable.of_compress {n : Nat} {α : Sort u} {o : Array Nat} {f : Nat → α} (hd : Descending o n) {q : Nat} (hq : q < n) (h : Stable (o.set! q o[o[q]!]!) n f) : Stable o n f

Replacing a parent by its parent preserves the original equations.

theorem Hex.GraphIso.Nauty.Orbit.flat_orbjoin {n : Nat} {o map : Array Nat} (hd : Descending o n) (hm : ∀ (i : Nat), i < n → map[i]! < n) : Flat (orbjoin o map n).fst n

After joining and compressing, every stored representative is a root.

theorem Hex.GraphIso.Nauty.Orbit.stable_orbjoin {n : Nat} {α : Sort u} {o map : Array Nat} {f : Nat → α} (hd : Descending o n) (hm : ∀ (i : Nat), i < n → map[i]! < n) (h : Stable (orbjoin o map n).fst n f) : Stable o n f ∧ ∀ (i : Nat), i < n → f map[i]! = f i

Any function constant on the final orbit cells is constant on every old cell and on every edge introduced by this join.

theorem Hex.GraphIso.Nauty.Orbit.Descending.orbjoin {n : Nat} {o map : Array Nat} (hd : Descending o n) (hm : ∀ (i : Nat), i < n → map[i]! < n) : Descending (Nauty.orbjoin o map n).fst n

theorem Hex.GraphIso.Nauty.Orbit.flat_fold {n : Nat} (maps : List (Array Nat)) : (∀ (γ : Array Nat), γ ∈ maps → ∀ (i : Nat), i < n → γ[i]! < n) → ∀ (o : Array Nat), Descending o n → Flat o n → Flat (List.foldl (fun (o γ : Array Nat) => (orbjoin o γ n).fst) o maps) n

Repeated joins preserve the property that entries are roots.

theorem Hex.GraphIso.Nauty.Orbit.stable_fold {n : Nat} {α : Sort u} {f : Nat → α} (maps : List (Array Nat)) : (∀ (γ : Array Nat), γ ∈ maps → ∀ (i : Nat), i < n → γ[i]! < n) → ∀ (o : Array Nat), Descending o n → Stable (List.foldl (fun (o γ : Array Nat) => (orbjoin o γ n).fst) o maps) n f → Stable o n f ∧ ∀ (γ : Array Nat), γ ∈ maps → ∀ (i : Nat), i < n → f γ[i]! = f i

A function constant on the final cells respects every generator edge.

theorem Hex.GraphIso.Nauty.Orbit.count_orbjoin {n : Nat} {o map : Array Nat} (hd : Descending o n) (hm : ∀ (i : Nat), i < n → map[i]! < n) : (orbjoin o map n).snd = List.countP (fun (i : Nat) => (orbjoin o map n).fst[i]! == i) (List.range n)

The count returned by the executed join and compression is exactly the number of roots in its returned array. This includes order zero.