mathlib documentation

tactic.omega.nat.neg_elim

source
@[simp]
def omega.nat.push_neg (a : 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 (a : omega.nat.preform) :
omega.nat.preform

NNF transformation

Equations
source
def omega.nat.is_nnf (a : 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) (a : 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 (a : omega.nat.preform) :
omega.nat.preform

Equations
source
theorem omega.nat.neg_free_neg_elim_core (p : omega.nat.preform) (a : 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 (a : 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)