theorem Hex.GraphIso.Nauty.keyCmp_bot_ne_gt {n : Nat} (b : Key n) : keyCmp { codes := [], rows := [] } b ≠ Ordering.gt

theorem Hex.GraphIso.Nauty.keyMax_bot_left {n : Nat} (b : Key n) : keyMax { codes := [], rows := [] } b = b

theorem Hex.GraphIso.Nauty.keyMax_bot_right {n : Nat} (b : Key n) : keyMax b { codes := [], rows := [] } = b

theorem Hex.GraphIso.Nauty.keyMax_assoc {n : Nat} (x y z : Key n) : keyMax (keyMax x y) z = keyMax x (keyMax y z)

theorem Hex.GraphIso.Nauty.keysMax_keyMax {n : Nat} (l : List (Key n)) (b c : Key n) : keysMax (keyMax b c) l = keyMax b (keysMax c l)

theorem Hex.GraphIso.Nauty.keyCmp_lt_of_nil {n : Nat} {b y : Key n} (hb : b.codes = []) (hy : y.codes ≠ []) : keyCmp b y = Ordering.lt

def Hex.GraphIso.Nauty.searchNode {n : Nat} (ctx : Ctx n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → Option (Key n) → Key n

Branch-and-bound maximum of the incumbent and this subtree's keys, expressed at this node's depth. The incumbent prunes children whose refinement code falls below its code here. Untrusted: results are validated by checkKey.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.searchNode ctx tcLevel 0 x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = x✝.getD { codes := [], rows := [] }

theorem Hex.GraphIso.Nauty.searchNode_eq {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (inc : Option (Key n)) : searchNode ctx tcLevel fuel level lab ptn active numcells inc = incMax inc (specNode ctx tcLevel fuel level lab ptn active numcells)

The pruned branch-and-bound recursion computes exactly the maximum of the incumbent and the unpruned subtree key: the code prune is lossless. No side conditions.

theorem Hex.GraphIso.Nauty.searchFold_eq {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (rsLab rsPtn : Array Nat) (tc numcells : Nat) (os : List Nat) (t : Key n) : List.foldl (fun (acc : Option (Key n)) (o : Nat) => some (searchNode ctx tcLevel fuel (level + 1) (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).snd.fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).snd.snd (numcells + 1) acc)) (some t) os = some (keysMax t (List.map (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells) os))

The child sweep from a present accumulator: folding the pruned child searches computes the running key maximum over the unpruned child keys.

theorem Hex.GraphIso.Nauty.searchFold_cons {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (rsLab rsPtn : Array Nat) (tc numcells o : Nat) (os : List Nat) (tail0 : Option (Key n)) : List.foldl (fun (acc : Option (Key n)) (o : Nat) => some (searchNode ctx tcLevel fuel (level + 1) (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).snd.fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).snd.snd (numcells + 1) acc)) tail0 (o :: os) = some (incMax tail0 (keysMax (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o) (List.map (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells) os)))

One unfolding of the child sweep from an arbitrary accumulator: the first child absorbs the incumbent, the rest fold from its result.

def Hex.GraphIso.Nauty.searchCanon (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Key n

The pruned search from an empty incumbent: a verified pruned evaluator of the spec key.

Equations

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

theorem Hex.GraphIso.Nauty.searchCanon_eq (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : searchCanon n g lab0 cellEnds = canonSpec n g lab0 cellEnds

theorem Hex.GraphIso.Nauty.searchCanon_key {n k : Nat} (G : Colored n k) : searchCanon n (rowsOf G) (initialPartition G).fst (initialPartition G).snd = canonSpecKey G

The pruned search computes the nauty-semantic canonical key.