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