HexGraphIso.Nauty.Sparse.CountProgress

structure Hex.GraphIso.Nauty.Sparse.CountTrace.Progress {n : Nat} (distance : Bool) (first last : Nat) (s : RefineSt n) (lab : Array Nat) (k : Nat) (c : Control n) (pos : Option Nat) (big : Nat) :

The completed part of a tail trace, expressed as a continuation for the still-unprocessed runs.

bounds : first ≤ k ∧ k < last
finish (out : Control n) : Tail distance lab s.hits first last k c pos big out → Result distance first last s lab out

Instances For

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Progress.next {distance : Bool} {first last n✝ : Nat} {s : RefineSt n✝} {lab : Array Nat} {k : Nat} {c : Control n✝} {pos : Option Nat} {big b : Nat} (h : Progress distance first last s lab k c pos big) (hk : k + 1 < last) (hr : Index.Run lab s.hits (k + 1) (last - 1) (k + 1) b) :

Progress distance first last s lab b (c.advance distance k s.hits[lab[k + 1]!]!) ((c.advance distance k s.hits[lab[k + 1]!]!).choose pos big (b - (k + 1) + 1)).fst ((c.advance distance k s.hits[lab[k + 1]!]!).choose pos big (b - (k + 1) + 1)).snd

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Progress.done {distance : Bool} {first last n✝ : Nat} {s : RefineSt n✝} {lab : Array Nat} {k : Nat} {c : Control n✝} {pos : Option Nat} {big : Nat} (h : Progress distance first last s lab k c pos big) (hk : last ≤ k + 1) :

Result distance first last s lab (c.finish distance first pos)

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Progress.initial {n first last : Nat} {lab : Array Nat} {v2 v3 w1 w2 : Nat} {distance : Bool} {s : RefineSt n} (hn : ∃ (q : Nat ), first ≤ q ∧ q < last ∧ s.hits[s.lab[q]!]! ≠ s.hits[s.lab[first]!]!) (hm : Minima lab s.hits first v2 v3 last w1 w2) (hv : v2 < v3) (he : v3 < last) :

have c := ((control s).base distance first w1 w2 v2).more distance first v2 v3; Progress distance first last s lab (v3 - 1) c.fst c.snd.fst c.snd.snd

structure Hex.GraphIso.Nauty.Sparse.CountTrace.Scan (lab hits : Array Nat) (start last upto consumed remaining : Nat) :

Constant prefix and stopping information for the executed inner run scan. The endpoint is inclusive; the two lengths come from its range cursor.

Instances For

Scan lab hits start last start 0 (last - start)

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Scan.step {lab hits : Array Nat} {start last upto consumed remaining : Nat} (h : Scan lab hits start last upto consumed (remaining + 1)) (he : hits[lab[upto + 1]!]! = hits[lab[start]!]!) :

Scan lab hits start last (upto + 1) (consumed + 1) remaining

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Scan.stop {lab hits : Array Nat} {start last upto consumed remaining : Nat} (h : Scan lab hits start last upto consumed remaining) (he : hits[lab[upto + 1]!]! ≠ hits[lab[start]!]!) :

Scan lab hits start last upto (last - start) 0

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Scan.run {lab hits : Array Nat} {start last upto : Nat} (h : Scan lab hits start last upto (last - start) 0) :

Index.Run lab hits start last start upto