structure Hex.GraphIso.Nauty.Sparse.RefinePrefix (level first : Nat) (before ptn : Array Nat) : Prop

A left-to-right cell pass leaves its unprocessed original partition suffix unchanged and begins that suffix at an original cell start.

• start : first = 0 ∨ before[first - 1]! ≤ level
• tail (q : Nat) : first ≤ q → ptn[q]! = before[q]!

theorem Hex.GraphIso.Nauty.Sparse.RefinePrefix.initial (ptn : Array Nat) (level : Nat) : RefinePrefix level 0 ptn ptn

theorem Hex.GraphIso.Nauty.Sparse.RefinePrefix.cell {level first : Nat} {before ptn : Array Nat} {len : Nat} (h : RefinePrefix level first before ptn) (hc : IsCell ptn level first len) : IsCell before level first len

theorem Hex.GraphIso.Nauty.Sparse.RefinePrefix.advance {level first : Nat} {before ptn : Array Nat} {len : Nat} (h : RefinePrefix level first before ptn) (hc : IsCell ptn level first len) : RefinePrefix level (first + len) before ptn

theorem Hex.GraphIso.Nauty.Sparse.RefinePrefix.counts {n : Nat} {s : RefineSt n} {level first : Nat} {before : Array Nat} (h : RefinePrefix level first before s.ptn) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (distance : Bool) : RefinePrefix level (s.cellend[first]! + 1) before (splitCounts level first distance s).ptn

def Hex.GraphIso.Nauty.Sparse.ConstantPrefix (n level upto : Nat) (key : Nat → Nat) (lab ptn : Array Nat) : Prop

Every complete cell in the processed prefix has a constant semantic key.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.ConstantPrefix.initial (lab ptn : Array Nat) (n level : Nat) (key : Nat → Nat) : ConstantPrefix n level 0 key lab ptn

theorem Hex.GraphIso.Nauty.Sparse.ConstantPrefix.singleton {n level first : Nat} {key : Nat → Nat} {lab ptn : Array Nat} (h : ConstantPrefix n level first key lab ptn) (hc : IsCell ptn level first 1) : ConstantPrefix n level (first + 1) key lab ptn

theorem Hex.GraphIso.Nauty.Sparse.ConstantPrefix.counts {n : Nat} {s : RefineSt n} {level first : Nat} {key : Nat → Nat} (h : ConstantPrefix n level first key s.lab s.ptn) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (hv : ∀ (v : Nat), v ∈ segN s.lab first (s.cellend[first]! + 1 - first) → s.hits[v]! = key v) (distance : Bool) : ConstantPrefix n level (s.cellend[first]! + 1) key (splitCounts level first distance s).lab (splitCounts level first distance s).ptn

theorem Hex.GraphIso.Nauty.Sparse.ConstantPrefix.done {n level : Nat} {key : Nat → Nat} {lab ptn : Array Nat} (h : ConstantPrefix n level n key lab ptn) (a len : Nat) : IsCell ptn level a len → a + len ≤ n → ∀ (q r : Nat), a ≤ q → q < a + len → a ≤ r → r < a + len → key lab[q]! = key lab[r]!