mathlib documentation

tactic.omega.nat.neg_elim

source
@[simp]
def omega.nat.push_neg  :
omega.nat.preform → omega.nat.preform

push_neg p returns the result of normalizing ¬ p by pushing the outermost negation all the way down, until it reaches either a negation or an atom

Equations
source
theorem omega.nat.push_neg_equiv {p : omega.nat.preform} :
(omega.nat.push_neg p).equiv (¬* p)
source
def omega.nat.nnf  :
omega.nat.preform → omega.nat.preform

NNF transformation

Equations
source
def omega.nat.is_nnf  :
omega.nat.preform → Prop

Asserts that the given preform is in NNF

Equations
source
theorem omega.nat.is_nnf_push_neg (p : omega.nat.preform) :
omega.nat.is_nnf p → omega.nat.is_nnf (omega.nat.push_neg p)
source
theorem omega.nat.is_nnf_nnf (p : omega.nat.preform) :
omega.nat.is_nnf (omega.nat.nnf p)
source
theorem omega.nat.nnf_equiv {p : omega.nat.preform} :
(omega.nat.nnf p).equiv p
source
@[simp]
def omega.nat.neg_elim_core  :
omega.nat.preform → omega.nat.preform
Equations
source
theorem omega.nat.neg_free_neg_elim_core (p : omega.nat.preform) :
omega.nat.is_nnf p → (omega.nat.neg_elim_core p).neg_free
source
theorem omega.nat.le_and_le_iff_eq {α : Type} [partial_order α] {a b : α} :
a ≤ b ∧ b ≤ a ↔ a = b
source
theorem omega.nat.implies_neg_elim_core {p : omega.nat.preform} :
p.implies (omega.nat.neg_elim_core p)
source
def omega.nat.neg_elim  :
omega.nat.preform → omega.nat.preform

Eliminate all negations in a preform

Equations
source
theorem omega.nat.neg_free_neg_elim {p : omega.nat.preform} :
(omega.nat.neg_elim p).neg_free
source
theorem omega.nat.implies_neg_elim {p : omega.nat.preform} :
p.implies (omega.nat.neg_elim p)