inductive Hex.GraphIso.Nauty.Sparse.Binary.Pass {n : Nat} (level stamp : Nat) : List Nat → RefineSt n → RefineSt n → Prop

A trace of the executed singleton-cell loop. Each head is a proper nontrivial cell at entry, and the cell contract describes its actual body. The generation is fixed while the touched cells are processed.

• nil {n level stamp : Nat} {s : RefineSt n} : Pass level stamp [] s s
• cons {n level stamp first : Nat} {s t : RefineSt n} {rest : List Nat} {u : RefineSt n} (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hf : first < s.cellend[first]!) (hb : s.cellend[first]! < n) (hstep : Cell level first (s.cellend[first]! + 1) (fun (v : Nat) => s.vmarks[v]! == stamp) s t) (ht : Pass level stamp rest t u) : Pass level stamp (first :: rest) s u

theorem Hex.GraphIso.Nauty.Sparse.Binary.Pass.append {level stamp : Nat} {xs : List Nat} {n✝ : Nat} {s t : RefineSt n✝} {ys : List Nat} {u : RefineSt n✝} (h : Pass level stamp xs s t) : Pass level stamp ys t u → Pass level stamp (xs ++ ys) s u

Consecutive portions of the actual touched-cell loop compose.

theorem Hex.GraphIso.Nauty.Sparse.Binary.Pass.valid {n level stamp : Nat} {xs : List Nat} {s t : RefineSt n} (h : Pass level stamp xs s t) : s.lab.toList.Perm (List.range n) → s.ptn.size = n → Index.Valid n s.lab s.ptn level s.cellstart s.cellend → t.lab.toList.Perm (List.range n) ∧ t.ptn.size = n ∧ Index.Valid n t.lab t.ptn level t.cellstart t.cellend

Every completed trace carries a labelling permutation and valid cache through all of its cells.