mathlib documentation

tactic.omega.nat.dnf

Equations

Return a list of bools that encodes which variables have nonzero coefficients

Equations

Return a list of bools that encodes which variables have nonzero coefficients in any one of the input terms

Equations
theorem omega.nat.holds_nonneg_consts_core {v : } (h1 : ∀ (x : ), 0 v x) (m : ) (bs : list bool) (t : omega.term) :

theorem omega.nat.holds_nonneg_consts {v : } {bs : list bool} (a : ∀ (x : ), 0 v x) (t : omega.term) :

theorem omega.nat.exists_clause_holds {v : } {p : omega.nat.preform} :
p.neg_freep.sub_freeomega.nat.preform.holds v p(∃ (c : omega.clause) (H : c omega.nat.dnf p), omega.clause.holds (λ (x : ), (v x)) c)

theorem omega.nat.exists_clause_sat {p : omega.nat.preform} :
p.neg_freep.sub_freep.sat(∃ (c : omega.clause) (H : c omega.nat.dnf p), c.sat)