structure Hex.GraphIso.Nauty.Sparse.FirstRef {n : Nat} (G : SparseGraph n) (tcLevel base : Nat) (root : RefineSt n) (st : State n) : Type

A frozen native ancestor's selected descent to the saved first leaf, including every literal cached call and its stored target and code slots.

• last : Nat
• leaf : RefineSt n
• path : List (Nat × Nat)
• codes : List Nat
• trace : CodePath G base root self.path self.last self.leaf self.codes
• selects : CodePath.Selects tcLevel self.trace
• targets : Targets st.firsttc base (List.map Prod.fst self.path)
• lab : self.leaf.lab = st.firstlab
• discrete : discreteAt self.leaf.ptn self.last n = true
• sentinel : st.firstcode[self.last + 1]! = codeSentinel
• stored : StoredCodes st.firstcode base self.codes

def Hex.GraphIso.Nauty.Sparse.FirstRef.congr {n : Nat} {G : SparseGraph n} {tcLevel base : Nat} {root : RefineSt n} {st out : State n} (h : FirstRef G tcLevel base root st) (he : SearchState.reference out = SearchState.reference st) : FirstRef G tcLevel base root out

Updating unrelated bookkeeping retains the complete native history.

Equations

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

def Hex.GraphIso.Nauty.Sparse.FirstRef.node {n : Nat} {G : SparseGraph n} {inf tcLevel fuel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) : FirstRef G tcLevel base root (Generic.node false (Graph.ofGraph G) inf tcLevel fuel level numcells st).snd

Equations

• h.node = h.congr ⋯

def Hex.GraphIso.Nauty.Sparse.FirstRef.sweep {n : Nat} {G : SparseGraph n} {first : Bool} {inf tcLevel fuel cfuel base level numcells tc tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {root : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) (hpast : Generic.Past first tv1 cursor) : FirstRef G tcLevel base root (Generic.sweep first (Graph.ofGraph G) inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Equations

• h.sweep hpast = h.congr ⋯

theorem Hex.GraphIso.Nauty.Sparse.firstRef_of_path {n k : Nat} {G : Sparse.Colored n k} {inf tcLevel fuel level numcells last : Nat} {st leaf : State n} (hn : 0 < n) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hl : 1 ≤ level) (h : NodeInv G level numcells st) (htsize : n < st.firsttc.size) (hcsize : n + 1 < st.firstcode.size) : ∃ (href : FirstRef G.graph tcLevel level (State.refined (Graph.ofGraph G.graph) level numcells st) (Generic.node true (Graph.ofGraph G.graph) inf tcLevel fuel level numcells st).snd), href.last = last

Completing the actual first-path call supplies a frozen native reference, retained after every later sibling and nonlocal return.