def Hex.GraphIso.Nauty.Sparse.Covers {n : Nat} (bound : Key n) (best : Option (Key n)) : Prop

A sparse subtree key is bounded by an installed native incumbent.

Equations

• Hex.GraphIso.Nauty.Sparse.Covers bound best = ∃ (b : Hex.GraphIso.Nauty.Sparse.Key n), best = some b ∧ bound.Le b

theorem Hex.GraphIso.Nauty.Sparse.Covers.grow {n : Nat} {bound : Key n} {before after : Option (Key n)} (h : Covers bound before) (hg : Grows before after) : Covers bound after

theorem Hex.GraphIso.Nauty.Sparse.Covers.mono {n : Nat} {a b : Key n} {best : Option (Key n)} (h : Covers b best) (hab : a.Le b) : Covers a best

theorem Hex.GraphIso.Nauty.Sparse.Covers.max {n : Nat} {a b : Key n} {best : Option (Key n)} (ha : Covers a best) (hb : Covers b best) : Covers (a.max b) best