@[instance_reducible]

instance Hex.GraphIso.Nauty.policy {n : Nat} : Generic.Policy (Search n) n

Equations

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

theorem Hex.GraphIso.Nauty.node_eq_generic {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : node first ctx inf tcLevel fuel level numcells st = Generic.node first ctx inf tcLevel fuel level numcells st

The direct node is the generic recursion at the nauty policy.

theorem Hex.GraphIso.Nauty.sweep_eq_generic {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell : VSet n) (index : Nat) (st : Search n) : sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell index st = Generic.sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell index st

The direct sweep is the generic recursion at the nauty policy.