def Hex.GraphIso.Nauty.pathCodes {n : Nat} (ctx : Ctx n) : Nat → RefineSt n → List (Nat × Nat) → List Nat

The refinement codes encountered along an individualization path, including its endpoint.

Equations

• Hex.GraphIso.Nauty.pathCodes ctx x✝¹ x✝ [] = [x✝.longcode]
• Hex.GraphIso.Nauty.pathCodes ctx x✝¹ x✝ ((tc, o) :: path) = x✝.longcode :: Hex.GraphIso.Nauty.pathCodes ctx (x✝¹ + 1) (Hex.GraphIso.Nauty.childSt ctx x✝¹ x✝ tc x✝.lab[tc + o]!) path

theorem Hex.GraphIso.Nauty.pathCodes_length {n : Nat} (ctx : Ctx n) (level : Nat) (st : RefineSt n) (path : List (Nat × Nat)) : (pathCodes ctx level st path).length = path.length + 1

A descent has one refinement code at every node.

def Hex.GraphIso.Nauty.StoredCodes (store : Array Nat) (base : Nat) (codes : List Nat) : Prop

A consecutive segment of an array stores the codes of a path.

Equations

• Hex.GraphIso.Nauty.StoredCodes store base codes = ∀ (i : Nat), i < codes.length → store[base + i]! = codes[i]!

theorem Hex.GraphIso.Nauty.StoredCodes.cons {store : Array Nat} {base code : Nat} {codes : List Nat} (head : store[base]! = code) (tail : StoredCodes store (base + 1) codes) : StoredCodes store base (code :: codes)

A stored head and a stored suffix form a single code segment.

theorem Hex.GraphIso.Nauty.StoredCodes.set_after {store : Array Nat} {base slot value : Nat} {codes : List Nat} (h : StoredCodes store base codes) (hafter : base + codes.length ≤ slot) : StoredCodes (store.set! slot value) base codes

A sentinel written after the path leaves every real code intact.

def Hex.GraphIso.Nauty.Selects {n : Nat} (ctx : Ctx n) (tcLevel : Nat) : Nat → RefineSt n → List (Nat × Nat) → Prop

Every target on a path is chosen by the unhinted specification rule.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Selects ctx tcLevel x✝¹ x✝ [] = True

theorem Hex.GraphIso.Nauty.DescPath.split_selects {n : Nat} {ctx : Ctx n} {tcLevel base level : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath ctx base root path level leaf) (hs : Selects ctx tcLevel base root path) {k : Nat} (hk : k ≤ path.length) : ∃ (middle : RefineSt n), DescPath ctx base root (List.take k path) (base + k) middle ∧ DescPath ctx (base + k) middle (List.drop k path) level leaf ∧ Selects ctx tcLevel (base + k) middle (List.drop k path)

Splitting a selected descent preserves the choices in its suffix.

theorem Hex.GraphIso.Nauty.Selects.append {n : Nat} {ctx : Ctx n} {tcLevel base level tc o : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath ctx base root path level leaf) (hs : Selects ctx tcLevel base root path) (htc : specTargetcell ctx leaf.lab leaf.ptn level tcLevel = tc) : Selects ctx tcLevel base root (path ++ [(tc, o)])

Appending a newly selected target extends an unhinted path.

theorem Hex.GraphIso.Nauty.Targets.drop {store : Array Int} {base : Nat} {xs : List Nat} (h : Targets store base xs) (k : Nat) : Targets store (base + k) (List.drop k xs)

A suffix of the target history starts at the corresponding deeper level.

theorem Hex.GraphIso.Nauty.Targets.eq {store : Array Int} {base : Nat} {xs ys : List Nat} (hx : Targets store base xs) (hy : Targets store base ys) (hlen : xs.length = ys.length) : xs = ys

Histories of equal length read from the same store are equal.

theorem Hex.GraphIso.Nauty.FollowsPerm.target {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level last : Nat} {root first current : RefineSt n} {path : List (Nat × Nat)} (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsmall : SubtreeOk ctx base root) (hfirst : DescPath ctx base root path last first) (hselected : Selects ctx tcLevel base root path) (hstored : Targets store base (List.map Prod.fst path)) (hcurrent : FollowsPerm ctx store base root level current) (hlevel : level ≤ last) (hdisc : ∀ (i : Nat), i < n → first.ptn[i]! ≤ last) (hopen : ∃ (i : Nat), i < n ∧ level < current.ptn[i]!) : Int.ofNat (specTargetcell ctx current.lab current.ptn level tcLevel) = store[level]!

The first path's target choices determine the next unhinted target of any non-discrete descent below a cheap ancestor that has followed the stored targets so far.