def Hex.GraphIso.Nauty.Sparse.Target.nontrivial (cs : List (Nat × Nat)) : List Nat

Nontrivial cell starts, in the partition's order.

Equations

• Hex.GraphIso.Nauty.Sparse.Target.nontrivial cs = List.map Prod.fst (List.filter (fun (p : Nat × Nat) => decide (p.fst < p.snd)) cs)

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.Target.nontrivial_append (cs ds : List (Nat × Nat)) : nontrivial (cs ++ ds) = nontrivial cs ++ nontrivial ds

structure Hex.GraphIso.Nauty.Sparse.Target.Scan (n : Nat) (ptn : Array Nat) (level used first : Nat) (out : List Nat) : Prop

Cursor invariant for the executed cell enumeration. The remaining recursive cell list is tied to the loop's actual remaining iteration count.

• used_le : used ≤ first
• first_le : first ≤ n
• boundary : first = 0 ∨ ptn[first - 1]! ≤ level
• before (a : Nat) : a ∈ out → a < first
• remaining : ∃ (seen : List (Nat × Nat)), cells ptn level n = seen ++ cells.go ptn level n (n - used) first ∧ out = nontrivial seen

theorem Hex.GraphIso.Nauty.Sparse.Target.Scan.initial (n : Nat) (ptn : Array Nat) (level : Nat) : Scan n ptn level 0 0 []

theorem Hex.GraphIso.Nauty.Sparse.Target.Scan.step {n level used first : Nat} {ptn : Array Nat} {out : List Nat} (h : Scan n ptn level used first out) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hu : used < n) (hf : first < n) : Scan n ptn level (used + 1) (cellEnd ptn level first + 1) (if first < cellEnd ptn level first then out ++ [first] else out)

theorem Hex.GraphIso.Nauty.Sparse.Target.Scan.finish {n level used first : Nat} {ptn : Array Nat} {out : List Nat} (h : Scan n ptn level used first out) (he : used = n ∨ first = n) : out = nontrivial (cells ptn level n)