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