Documentation

HexGraphIso.Nauty.Sparse.Touched

structure Hex.GraphIso.Nauty.Sparse.Touched (n stamp : Nat) (before marks touched : Array Nat) (seen : List Nat) :

A generation-marked scan records each nonsentinel cell exactly once. seen includes all observed keys, including the singleton sentinel.

Instances For
    theorem Hex.GraphIso.Nauty.Sparse.Touched.empty {n stamp : Nat} {before : Array Nat} (h : Scratch.Marks n stamp before) :
    Touched n stamp before before #[] []
    theorem Hex.GraphIso.Nauty.Sparse.Touched.marked {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) :
    marks[k]! = stamp + 1 ↔ k ∈ seen

    A current-generation mark is equivalent to prior occurrence in the scan.

    theorem Hex.GraphIso.Nauty.Sparse.Touched.present {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) :
    marks[k]! = stamp + 1 ↔ k ∈ touched.toList
    theorem Hex.GraphIso.Nauty.Sparse.Touched.sentinel {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} (h : Touched n stamp before marks touched seen) :
    Touched n stamp before marks touched (seen ++ [n])

    Singleton cells are skipped without touching generation marks.

    theorem Hex.GraphIso.Nauty.Sparse.Touched.repeated {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) (hm : marks[k]! = stamp + 1) :
    Touched n stamp before marks touched (seen ++ [k])

    Repeated neighbours of the same cell do not add duplicate work.

    theorem Hex.GraphIso.Nauty.Sparse.Touched.fresh {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) (hm : marks[k]! ≠ stamp + 1) :
    Touched n stamp before (marks.setIfInBounds k (stamp + 1)) (touched.push k) (seen ++ [k])

    First touch marks the cell and appends it exactly once.