Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
Final term is not finished(T ∧ ¬(p ∨ ¬q) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.truezeroand(¬(p ∨ ¬q) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(¬p ∧ ¬¬q ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(¬p ∧ q ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.defequiv(¬p ∧ q ∧ ((r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.absorpor(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.oroverand(¬p ∧ q ∧ (r ∨ ¬s) ∧ (s ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.complor(¬p ∧ q ∧ (r ∨ ¬s) ∧ T) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.truezeroand(¬p ∧ q ∧ (r ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.andoveror(¬p ∧ ((q ∧ r) ∨ (q ∧ ¬s))) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.andoveror(¬p ∧ q ∧ r) ∨ (¬p ∧ q ∧ ¬s) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))