theorem
Hex.GraphIso.Nauty.StoredCodes.append
{store : Array Nat}
{base : Nat}
{xs ys : List Nat}
(hx : StoredCodes store base xs)
(hy : StoredCodes store (base + xs.length) ys)
:
StoredCodes store base (xs ++ ys)
Adjacent stored code segments concatenate without changing their literal array indices.
theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.comparison
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel last : Nat}
{f : Frame n}
{leaf : State n}
(h : FirstEntry G f)
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf)
:
The actual first descent extends the incoming stored prefix to a complete first-leaf code sequence. Both comparison machines are initialized from those literal writes at arbitrary entry depth.
theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.returned
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel last : Nat}
{f : Frame n}
{leaf : State n}
(h : FirstEntry G f)
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf)
(hf : n + 1 ≤ f.level + fuel)
:
The complete first call supplies readable incumbent codes with the entry's actual prefix. Leaf comparisons and prefix equality are derived from its executed descent, not supplied as separate proof obligations.