structure Hex.GraphIso.Nauty.Max.Frame (n : Nat) : Type

A frozen node and the refinement codes preceding its entry.

• level : Nat
• numcells : Nat
• codes : List Nat
• entry : Search n

def Hex.GraphIso.Nauty.Max.Frame.key {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (f : Frame n) : Key n

The full specification subtree at a frozen node.

Equations

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

def Hex.GraphIso.Nauty.Max.Frame.code {n : Nat} (ctx : Ctx n) (f : Frame n) : Nat

The first refinement code of a frozen node.

Equations

• Hex.GraphIso.Nauty.Max.Frame.code ctx f = (Hex.GraphIso.Nauty.refine ctx f.level f.entry.lab f.entry.ptn f.entry.active f.numcells).longcode

theorem Hex.GraphIso.Nauty.Max.Frame.tail {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {f : Frame n} (hlevel : f.level ≤ n) : ∃ (tail : Key n), key ctx tcLevel f = prefixKey (f.codes ++ [code ctx f]) tail

The specification of a nonexhausted frame begins with its refinement code.

def Hex.GraphIso.Nauty.Max.Frame.Witness {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (f : Frame n) (best : Option (Key n)) : Prop

Either a specific ancestor subtree is covered, or a frozen downward comparison bounds every extension of its first refinement code.

Equations

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

theorem Hex.GraphIso.Nauty.Max.Frame.Witness.resolve {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {f : Frame n} {best : Option (Key n)} (h : Witness ctx tcLevel f best) (hlevel : f.level ≤ n) : Generic.Covers (key ctx tcLevel f) best

Both return justifications cover the actual frozen specification subtree.

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Max.Frames (n : Nat) : Type

Frozen ancestor subtrees are indexed by their receiving sweep level.

Equations

• Hex.GraphIso.Nauty.Max.Frames n = (Nat → Option (Hex.GraphIso.Nauty.Max.Frame n))

def Hex.GraphIso.Nauty.Max.Frames.insert {n : Nat} (frames : Frames n) (f : Frame n) : Frames n

Install the current node's subtree at its receiving parent.

Equations

• frames.insert f level = if level = f.level - 1 then some f else frames level

def Hex.GraphIso.Nauty.Max.Witness {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (frames : Frames n) (target : Nat) (best : Option (Key n)) : Prop

A nonlocal return carries a justification for the ancestor it names.

Equations

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

theorem Hex.GraphIso.Nauty.Max.Witness.resolve {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {frames : Frames n} {f : Frame n} {best : Option (Key n)} (h : Witness ctx tcLevel (frames.insert f) (f.level - 1) best) : Generic.Covers (Frame.key ctx tcLevel f) best

A return to the current node's parent resolves its own frozen key.

theorem Hex.GraphIso.Nauty.Max.Witness.below {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {frames : Frames n} {f : Frame n} {best : Option (Key n)} (ht : target < f.level - 1) : Witness ctx tcLevel (frames.insert f) target best ↔ Witness ctx tcLevel frames target best

Pushing a descendant frame leaves every earlier ancestor unchanged.