def Hex.GraphIso.Nauty.Max.verdict {n k : Nat} (G : Colored n k) (tcLevel level numcells : Nat) (st : Search n) : Leaf

The actual classification used by an off-path node.

Equations

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

def Hex.GraphIso.Nauty.Max.NodeRule {n k : Nat} (G : Colored n k) (tcLevel : Nat) (first : Bool) (guard : Nat → Nat → Search n → Prop) : Prop

One node branch, with only the smaller sweep's contract assumed.

Equations

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

def Hex.GraphIso.Nauty.Max.SweepRule {n k : Nat} (G : Colored n k) (tcLevel : Nat) (visits : Bool) : Prop

One sweep branch, with only its smaller node and suffix contracts assumed.

Equations

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

def Hex.GraphIso.Nauty.Max.NodeTraceRule {n k : Nat} (G : Colored n k) (tcLevel : Nat) : Prop

The node's generator conclusion uses the same smaller sweep contract as its key bounds.

Equations

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

def Hex.GraphIso.Nauty.Max.SweepTraceRule {n k : Nat} (G : Colored n k) (tcLevel : Nat) : Prop

The sweep's accumulated trace is preserved by its actual smaller child and suffix calls, in the same induction as maximum coverage.

Equations

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

structure Hex.GraphIso.Nauty.Max.Rules {n k : Nat} (G : Colored n k) (tcLevel : Nat) : Prop

Local maximum obligations for every node verdict and both sweep branches, assuming only the contracts of smaller recursive calls.

• first_leaf : NodeRule G tcLevel true fun (level numcells : Nat) (st : Search n) => (Generic.prepareFirst { g := rowsOf G } tcLevel level numcells st).fst = n
• first_branch : NodeRule G tcLevel true fun (level numcells : Nat) (st : Search n) => (Generic.prepareFirst { g := rowsOf G } tcLevel level numcells st).fst ≠ n
• other_branch : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.internal
• auto_first : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.autoFirst
• auto_canon : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.autoCanon
• better (sr : Nat) : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.better sr
• bad : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.bad
• visit : SweepRule G tcLevel true
• skip : SweepRule G tcLevel false
• finish (fuel cfuel : Nat) (first : Bool) (level numcells tc tv1 : Nat) (cell : VSet n) (index : Nat) (st : Search n) : (keyContract G tcLevel).sweepPost fuel cfuel first level numcells tc tv1 none cell index st (Generic.Exit.done, index, st)
• node_trace : NodeTraceRule G tcLevel
• sweep_trace : SweepTraceRule G tcLevel

theorem Hex.GraphIso.Nauty.Max.Rules.calls {n k : Nat} {G : Colored n k} {tcLevel : Nat} (h : Rules G tcLevel) : Generic.CallPolicy { g := rowsOf G } (n + 2) tcLevel (contract G tcLevel)

The exhaustive branch obligations instantiate the single generic recursion.