def Hex.GraphIso.Nauty.Sparse.Target.FirstMax (score : Nat → Nat) (xs : List Nat) (winner : Nat) : Prop

The first occurrence of a maximal score: preceding scores are strictly smaller, and following scores are no larger.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Target.FirstMax.mem {score : Nat → Nat} {xs : List Nat} {winner : Nat} (h : FirstMax score xs winner) : winner ∈ xs

theorem Hex.GraphIso.Nauty.Sparse.Target.FirstMax.bound {score : Nat → Nat} {xs : List Nat} {winner v : Nat} (h : FirstMax score xs winner) (hv : v ∈ xs) : score v ≤ score winner

theorem Hex.GraphIso.Nauty.Sparse.Target.FirstMax.cons_lt {score : Nat → Nat} {xs : List Nat} {winner v : Nat} (h : FirstMax score xs winner) (hv : score v < score winner) : FirstMax score (v :: xs) winner

theorem Hex.GraphIso.Nauty.Sparse.Target.FirstMax.insert {score : Nat → Nat} {xs : List Nat} {winner b v : Nat} (h : FirstMax score (b :: xs) winner) (hv : score v ≤ score b) : FirstMax score (b :: v :: xs) winner

A candidate no better than the current representative can be skipped without changing the earliest maximal candidate.

theorem Hex.GraphIso.Nauty.Sparse.Target.best_max (keys : List Nat) (score : Nat → Nat) (empty : Nat) (hne : keys ≠ []) : FirstMax score keys (best keys score empty)

The strict comparison in the executed selection fold chooses precisely the first cell with maximum score.