@[simp]
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
- omega.nat.push_neg (p.and q) = (omega.nat.push_neg p).or (omega.nat.push_neg q)
- omega.nat.push_neg (p.or q) = (omega.nat.push_neg p).and (omega.nat.push_neg q)
- omega.nat.push_neg p.not = p
- omega.nat.push_neg (omega.nat.preform.le a a_1) = (omega.nat.preform.le a a_1).not
- omega.nat.push_neg (omega.nat.preform.eq a a_1) = (omega.nat.preform.eq a a_1).not
NNF transformation
Equations
- omega.nat.nnf (p.and q) = (omega.nat.nnf p).and (omega.nat.nnf q)
- omega.nat.nnf (p.or q) = (omega.nat.nnf p).or (omega.nat.nnf q)
- omega.nat.nnf p.not = omega.nat.push_neg (omega.nat.nnf p)
- omega.nat.nnf (omega.nat.preform.le a a_1) = omega.nat.preform.le a a_1
- omega.nat.nnf (omega.nat.preform.eq a a_1) = omega.nat.preform.eq a a_1
Asserts that the given preform is in NNF
Equations
- omega.nat.is_nnf (p.and q) = (omega.nat.is_nnf p ∧ omega.nat.is_nnf q)
- omega.nat.is_nnf (p.or q) = (omega.nat.is_nnf p ∧ omega.nat.is_nnf q)
- omega.nat.is_nnf (a.and a_1).not = false
- omega.nat.is_nnf (a.or a_1).not = false
- omega.nat.is_nnf a.not.not = false
- omega.nat.is_nnf (omega.nat.preform.le t s).not = true
- omega.nat.is_nnf (omega.nat.preform.eq t s).not = true
- omega.nat.is_nnf (omega.nat.preform.le t s) = true
- omega.nat.is_nnf (omega.nat.preform.eq t s) = true
@[simp]
Equations
- omega.nat.neg_elim_core (p.and q) = (omega.nat.neg_elim_core p).and (omega.nat.neg_elim_core q)
- omega.nat.neg_elim_core (p.or q) = (omega.nat.neg_elim_core p).or (omega.nat.neg_elim_core q)
- omega.nat.neg_elim_core (a.and a_1).not = (a.and a_1).not
- omega.nat.neg_elim_core (a.or a_1).not = (a.or a_1).not
- omega.nat.neg_elim_core a.not.not = a.not.not
- omega.nat.neg_elim_core (omega.nat.preform.le t s).not = omega.nat.preform.le s.add_one t
- omega.nat.neg_elim_core (omega.nat.preform.eq t s).not = (omega.nat.preform.le t.add_one s).or (omega.nat.preform.le s.add_one t)
- omega.nat.neg_elim_core (omega.nat.preform.le a a_1) = omega.nat.preform.le a a_1
- omega.nat.neg_elim_core (omega.nat.preform.eq a a_1) = omega.nat.preform.eq a a_1
Eliminate all negations in a preform