A native descent carrying each executed refinement code, including the terminal node's code. The sentinel is recorded separately by leaf installation. Scratch arguments are the actual arguments at each step.
- refl {n : Nat} {G : SparseGraph n} (level : Nat) (st : RefineSt n) : CodePath G level st [] level st [st.longcode]
- step {n : Nat} {G : SparseGraph n} {level last : Nat} {st leaf : RefineSt n} {path : List (Nat × Nat)} {codes : List Nat} (tc len o : Nat) (scratch : Scratch) (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (hs : Scratch.Bounded n scratch) (tail : CodePath G (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) path last leaf codes) : CodePath G level st ((tc, o) :: path) last leaf (st.longcode :: codes)
Instances For
def
Hex.GraphIso.Nauty.Sparse.CodePath.Selects
{n : Nat}
{G : SparseGraph n}
(tcLevel : Nat)
{base last : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
{codes : List Nat}
:
Every step follows the native unhinted target rule at its actual refined state. The first-path construction establishes this predicate.
Equations
- One or more equations did not get rendered due to their size.
- Hex.GraphIso.Nauty.Sparse.CodePath.Selects tcLevel (Hex.GraphIso.Nauty.Sparse.CodePath.refl x✝¹ x✝) = True
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.CodePath.descent
{n : Nat}
{G : SparseGraph n}
{base last : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
{codes : List Nat}
(h : CodePath G base root path last leaf codes)
:
DescPath G base root path last leaf
Forgetting codes retains the exact same native descent.