theorem
Hex.GraphIso.Nauty.joinTest_iff_first
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level : Nat}
(heq : Equitable ctx level lab ptn)
{c d : Nat × Nat}
(hc : c ∈ cells ptn level n)
(hd : d ∈ cells ptn level n)
:
On an equitable pair of cells, nauty's representative test agrees with the specification's count-multiset test.
theorem
Hex.GraphIso.Nauty.bestcellRow_eq_spec
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level : Nat}
(heq : Equitable ctx level lab ptn)
(hlab : LabOk lab n)
(hlsz : lab.size = n)
(hpsz : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
{startArr : Array Nat}
(hstart : ∀ (v : Nat), v < startArr.size → ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ startArr[v]! = p.fst)
{v2 : Nat}
(hv2 : v2 < startArr.size)
(vs : List Nat)
(bucket : Array Nat)
:
The executable and specification row counters take the same branches on an equitable partition.
theorem
Hex.GraphIso.Nauty.bestcellRows_eq_spec
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level : Nat}
(heq : Equitable ctx level lab ptn)
(hlab : LabOk lab n)
(hlsz : lab.size = n)
(hpsz : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
{startArr : Array Nat}
(hstart : ∀ (v : Nat), v < startArr.size → ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ startArr[v]! = p.fst)
(vs : List Nat)
(bucket : Array Nat)
:
(∀ (v : Nat), v ∈ vs → v < startArr.size) →
bestcellRows ctx lab ptn level startArr vs bucket = specBestcellRows ctx lab ptn level startArr vs bucket
Folding the row counters over all nonsingleton cells produces the same bucket on an equitable partition.
theorem
Hex.GraphIso.Nauty.bestcell_eq_spec
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level : Nat}
(heq : Equitable ctx level lab ptn)
(hlab : LabOk lab n)
(hlsz : lab.size = n)
(hpsz : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
:
On an equitable partition, nauty's bestcell agrees with the
specification's representative-independent form.
theorem
Hex.GraphIso.Nauty.targetcell_eq_spec_of_inadmissible
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level tcLevel : Nat}
(heq : Equitable ctx level lab ptn)
(hlab : LabOk lab n)
(hlsz : lab.size = n)
(hpsz : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
(hint : Int)
(hbad : ¬(hint ≥ 0 ∧ ptn[hint.toNat]! > level ∧ ((hint == 0) = true ∨ ptn[hint.toNat - 1]! ≤ level)))
:
If a history-dependent hint is inadmissible, the executable falls through to the specification's target-cell policy.
theorem
Hex.GraphIso.Nauty.targetcell_eq_spec
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level tcLevel : Nat}
(heq : Equitable ctx level lab ptn)
(hlab : LabOk lab n)
(hlsz : lab.size = n)
(hpsz : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
:
With no history-dependent hint, the executable and specification target-cell choices agree on an equitable partition.
theorem
Hex.GraphIso.Nauty.maketargetcell_eq_spec
{n : Nat}
{ctx : Ctx n}
{lab ptn : Array Nat}
{level tcLevel : Nat}
(heq : Equitable ctx level lab ptn)
(hlab : LabOk lab n)
(hlsz : lab.size = n)
(hpsz : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
:
The complete unhinted target-cell record agrees with the specification on an equitable partition.