theorem Hex.GraphIso.Nauty.Sparse.indexCells_valid {n : Nat} (lab ptn starts ends : Array Nat) (level : Nat) (hptn : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hbound : ∀ (i : Nat), i < n → lab[i]! < n) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hs : starts.size = n) (he : ends.size = n) : Index.Valid n lab ptn level (indexCells n lab ptn level starts ends).fst (indexCells n lab ptn level starts ends).snd

The executed bounded cell walk fills every cell index. It needs only a bounded injective labelling and a partition closed at its last position.

theorem Hex.GraphIso.Nauty.Sparse.indexCells_label {n : Nat} (lab ptn starts ends : Array Nat) (level : Nat) (l : Label n) (hl : Label.ofArray? n lab = some l) (hptn : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hs : starts.size = n) (he : ends.size = n) : Index.Valid n lab ptn level (indexCells n lab ptn level starts ends).fst (indexCells n lab ptn level starts ends).snd

A checked public label supplies the bounded, injective raw labelling.