Documentation

HexGraphIso.Nauty.Sparse.Minima

source
structure Hex.GraphIso.Nauty.Sparse.Minima (lab hits : Array Nat) (first v2 v3 upto w1 w2 : Nat) :
Prop

The first two constant-count fragments and the larger counts already scanned by nauty's three-way insertion. The second fragment may be empty.

Instances For
    source
    theorem Hex.GraphIso.Nauty.Sparse.Minima.initial {lab hits : Array Nat} {first upto w1 w2 : Nat} (hb : first < upto) (hk : w1 < w2) (hm : ∀ (q : Nat), first ≤ q → q < upto → hits[lab[q]!]! = w1) :
    Minima lab hits first upto upto upto w1 w2
    source
    theorem Hex.GraphIso.Nauty.Sparse.Minima.hit_min {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hb : upto < lab.size) (hk : hits[lab[upto]!]! = w1) :
    Minima (((lab.set! upto lab[v3]!).set! v3 lab[v2]!).set! v2 lab[upto]!) hits first (v2 + 1) (v3 + 1) (upto + 1) w1 w2
    source
    theorem Hex.GraphIso.Nauty.Sparse.Minima.hit_second {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hb : upto < lab.size) (hk : hits[lab[upto]!]! = w2) :
    Minima ((lab.set! upto lab[v3]!).set! v3 lab[upto]!) hits first v2 (v3 + 1) (upto + 1) w1 w2
    source
    theorem Hex.GraphIso.Nauty.Sparse.Minima.new_min {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hb : upto < lab.size) (hk : hits[lab[upto]!]! < w1) :
    Minima (((lab.set! upto lab[v2]!).set! v2 lab[first]!).set! first lab[upto]!) hits first (first + 1) (v2 + 1) (upto + 1) hits[lab[upto]!]! w1
    source
    theorem Hex.GraphIso.Nauty.Sparse.Minima.new_second {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hb : upto < lab.size) (hlo : w1 < hits[lab[upto]!]!) (hhi : hits[lab[upto]!]! < w2) :
    Minima ((lab.set! upto lab[v2]!).set! v2 lab[upto]!) hits first v2 (v2 + 1) (upto + 1) w1 hits[lab[upto]!]!
    source
    theorem Hex.GraphIso.Nauty.Sparse.Minima.above {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hk : w2 < hits[lab[upto]!]!) :
    Minima lab hits first v2 v3 (upto + 1) w1 w2