Partition effects and canonical-reference effects share the same entry conditions, including calls truncated by fuel exhaustion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.canon_finish
{n k : Nat}
{G : Colored n k}
{fuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hnext : (canonContract G).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells tc size : Nat)
(cell : VSet n)
(st : Search n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
:
A node's completed sweep retains or installs its canonical reference.
theorem
Hex.GraphIso.Nauty.canon_node
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hn0 : 0 < n)
(hnext : (canonContract G).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells : Nat)
(st : Search n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
:
CanonOut level st (Generic.nodeStep ctx tcLevel next first level numcells st).snd
Local node operations retain the reference or install one in the refined partition, and refinement transports that fact to the entry.
theorem
Hex.GraphIso.Nauty.canon_advance
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hn0 : 0 < n)
(hnext : (canonContract G).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(base out : Search n)
(exit : Exit)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells base)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell base)
(hout : SearchOut G level level base out)
(hcanon : CanonOut level base out)
:
CanonOut level base (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd
An intermediate sweep transports the child's reference; a receiving sweep recovers the parent before composing the remaining siblings.
theorem
Hex.GraphIso.Nauty.canon_sweep
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{descend : Generic.NodeFn (Search n)}
{next : Generic.SweepFn (Search n) n}
(hn0 : 0 < n)
(hdescend : (canonContract G).nodeValid fuel descend)
(hnext : (canonContract G).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(st : Search n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(htv : cell.mem tv = true)
:
CanonOut level st (Generic.sweepStep (n + 2) descend next first level numcells tc tv1 tv cell index st).snd.snd
One child and the remaining sweep compose their canonical effects, including first-child bookkeeping and all non-local exits.
theorem
Hex.GraphIso.Nauty.canonPolicy
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel : Nat)
(hn0 : 0 < n)
:
Generic.SoundPolicy ctx (n + 2) tcLevel (canonContract G)
Canonical-reference tracking is an instance of the common policy induction.
theorem
Hex.GraphIso.Nauty.sweep_canon
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
(first : Bool)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(hcursor : ∀ (v : Nat), cursor = some v → cell.mem v = true)
:
A whole sweep couples its stored canonical labelling to its ancestor counter.