mathlib documentation

tactic.omega.nat.dnf

DNF transformation #

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) (H : t omega.nat.nonneg_consts_core m bs) :
theorem omega.nat.holds_nonneg_consts {v : } {bs : list bool} :
(∀ (x : ), 0 v x)∀ (t : omega.term), t omega.nat.nonneg_consts bs0 omega.term.val v t
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)