def Hex.GraphIso.Nauty.Sparse.OrbitReplay {n : Nat} (st : State n) : Prop

The native orbit array and count are exactly the successive joins of the full emitted trace. This is an invariant of the executed bookkeeping, including redundant admissions, rather than another orbit computation.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.admit_numorbits {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).numorbits = (orbjoin st.orbits st.workperm n).snd

theorem Hex.GraphIso.Nauty.Sparse.leafExit_numorbits {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.numorbits = match leaf with | Generic.Leaf.autoFirst => (orbjoin st.orbits st.workperm n).snd | Generic.Leaf.autoCanon => (orbjoin st.orbits st.workperm n).snd | x => st.numorbits

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.congr {n : Nat} {st out : State n} (h : OrbitReplay st) (ht : out.genTrace = st.genTrace) (ho : out.orbits = st.orbits) (hc : out.numorbits = st.numorbits) : OrbitReplay out

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.initial {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : OrbitReplay (Sparse.initial g lab ends)

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.admit {n : Nat} {st : State n} (h : OrbitReplay st) : OrbitReplay (Nauty.admit st)

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.leaf {n : Nat} {st : State n} (h : OrbitReplay st) (leaf : Leaf) (level : Nat) : OrbitReplay (leafExit leaf level st).snd

theorem Hex.GraphIso.Nauty.Sparse.orbitReplayPolicy {n : Nat} (g : Graph n) (inf tcLevel : Nat) : Generic.Preserve g inf tcLevel OrbitReplay

Literal preparation, cache invalidation and level recovery preserve both orbit fields and their exact relationship to the trace.

theorem Hex.GraphIso.Nauty.Sparse.node_orbitReplay {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) (h : OrbitReplay st) : OrbitReplay (Generic.node first g inf tcLevel fuel level numcells st).snd

Every complete or truncated native node retains the exact orbit join sequence. The statement needs no semantic assumption about the graph.

theorem Hex.GraphIso.Nauty.Sparse.runColored_orbitReplay {n k : Nat} (G : Sparse.Colored n k) : OrbitReplay (runColored G)

The actual final pointers and count are the joins of precisely the emitted sparse generator arrays, including for the empty graph.

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.orbits {n : Nat} {st : State n} (h : OrbitReplay st) : st.orbits = List.foldl (fun (o gamma : Array Nat) => (orbjoin o gamma n).fst) (Array.ofFn Fin.val) st.genTrace.toList

Forgetting the count in the literal join sequence gives the same array fold used in the abstract orbit closure lemmas.