def Hex.GraphIso.Nauty.SearchState.reference {n : Nat} {κ : Type} (st : SearchState n κ) : Array Nat × Array Int × Array Nat

The saved first-path codes, target positions, and leaf labelling.

Equations

• st.reference = (st.firstcode, st.firsttc, st.firstlab)

theorem Hex.GraphIso.Nauty.pushAuto_reference {n : Nat} {κ : Type} (st : SearchState n κ) (pair : VSet n × VSet n) : (pushAuto st pair).reference = st.reference

Workspace insertion preserves the first-path reference.

theorem Hex.GraphIso.Nauty.scatter_reference {n : Nat} {κ : Type} (ref : Array Nat) (st : SearchState n κ) : (scatter ref st).reference = st.reference

Scratch construction preserves the first-path reference.

theorem Hex.GraphIso.Nauty.classify_reference {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : SearchState.reference (classify ctx level numcells st).snd = SearchState.reference st

Classifying a node never replaces the first-path reference.

theorem Hex.GraphIso.Nauty.admit_reference {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).reference = st.reference

Recording a generator preserves the first-path reference.

theorem Hex.GraphIso.Nauty.pruneReturn_reference {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (pruneReturn level st).snd.reference = st.reference

Pruning past a leaf preserves the first-path reference.

theorem Hex.GraphIso.Nauty.leafExit_reference {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.reference = st.reference

Off-path leaf processing never replaces the first-path reference.

theorem Hex.GraphIso.Nauty.referencePolicy {n : Nat} (ctx : Ctx n) (inf tcLevel : Nat) : Generic.ReferencePolicy ctx inf tcLevel SearchState.reference

The search's off-path operations preserve all first-path reference fields.

theorem Hex.GraphIso.Nauty.node_reference {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : SearchState.reference (node false ctx inf tcLevel fuel level numcells st).snd = SearchState.reference st

Off-path search preserves the saved first-path codes, targets, and leaf.

theorem Hex.GraphIso.Nauty.sweep_reference {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : Search n) (hpast : Generic.Past first tv1 cursor) : SearchState.reference (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd = SearchState.reference st

A sweep past its first child preserves the saved first-path reference.