A descent through literal native child calls. Each step records its target, selected offset and actual bounded scratch argument; no fresh-cache substitution or dense refinement appears in the relation.
- refl {n : Nat} {G : SparseGraph n} (level : Nat) (st : RefineSt n) : DescPath G level st [] level st
- step {n : Nat} {G : SparseGraph n} {level last : Nat} {st leaf : RefineSt n} {path : List (Nat × 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 : DescPath G (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) path last leaf) : DescPath G level st ((tc, o) :: path) last leaf
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.child_shape
{n : Nat}
{G : SparseGraph n}
{level : Nat}
{s : RefineSt n}
(h : Ready G level s)
{tc len o : Nat}
(hc : IsCell s.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ho : o < len)
(scratch : Scratch)
(hs : Scratch.Bounded n scratch)
(hshape : NodeShape n level s.ptn)
:
NodeShape n (level + 1) (RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + o]! scratch).ptn
The precise cached child call preserves the shape supplied by a cheap ancestor: individualization and native refinement only add boundaries.
theorem
Hex.GraphIso.Nauty.Sparse.DescPath.ready
{n : Nat}
{G : SparseGraph n}
{base last : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
(h : DescPath G base root path last leaf)
(hr : RefineSt.Ready G base root)
:
RefineSt.Ready G last leaf