Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
Final term is not finished¬(F ∨ ¬(¬(q → p) ↔ ((r ↔ s) ∨ ¬s)) ∨ F)
⇒ logic.propositional.defimpl¬(F ∨ ¬(¬(¬q ∨ p) ↔ ((r ↔ s) ∨ ¬s)) ∨ F)
⇒ logic.propositional.demorganor¬(F ∨ ¬((¬¬q ∧ ¬p) ↔ ((r ↔ s) ∨ ¬s)) ∨ F)
⇒ logic.propositional.falsezeroor¬(F ∨ ¬((¬¬q ∧ ¬p) ↔ ((r ↔ s) ∨ ¬s)))
⇒ logic.propositional.notnot¬(F ∨ ¬((q ∧ ¬p) ↔ ((r ↔ s) ∨ ¬s)))
⇒ logic.propositional.defequiv¬(F ∨ ¬((q ∧ ¬p) ↔ ((r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬s)))
⇒ logic.propositional.absorpor¬(F ∨ ¬((q ∧ ¬p) ↔ ((r ∧ s) ∨ ¬s)))
⇒ logic.propositional.oroverand¬(F ∨ ¬((q ∧ ¬p) ↔ ((r ∨ ¬s) ∧ (s ∨ ¬s))))
⇒ logic.propositional.complor¬(F ∨ ¬((q ∧ ¬p) ↔ ((r ∨ ¬s) ∧ T)))
⇒ logic.propositional.truezeroand¬(F ∨ ¬((q ∧ ¬p) ↔ (r ∨ ¬s)))
⇒ logic.propositional.defequiv¬(F ∨ ¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ (¬(q ∧ ¬p) ∧ ¬(r ∨ ¬s))))
⇒ logic.propositional.demorganand¬(F ∨ ¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ ¬¬p) ∧ ¬(r ∨ ¬s))))
⇒ logic.propositional.notnot¬(F ∨ ¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ p) ∧ ¬(r ∨ ¬s))))
⇒ logic.propositional.demorganor¬(F ∨ ¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ p) ∧ ¬r ∧ ¬¬s)))
⇒ logic.propositional.notnot¬(F ∨ ¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ p) ∧ ¬r ∧ s)))
⇒ logic.propositional.demorganor¬(F ∨ (¬(q ∧ ¬p ∧ (r ∨ ¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s)))
⇒ logic.propositional.gendemorganand¬(F ∨ ((¬q ∨ ¬¬p ∨ ¬(r ∨ ¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s)))
⇒ logic.propositional.notnot¬(F ∨ ((¬q ∨ p ∨ ¬(r ∨ ¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s)))
⇒ logic.propositional.demorganor¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ ¬¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s)))
⇒ logic.propositional.notnot¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s)))
⇒ logic.propositional.gendemorganand¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ (¬(¬q ∨ p) ∨ ¬¬r ∨ ¬s)))
⇒ logic.propositional.notnot¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ (¬(¬q ∨ p) ∨ r ∨ ¬s)))
⇒ logic.propositional.demorganor¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ((¬¬q ∧ ¬p) ∨ r ∨ ¬s)))
⇒ logic.propositional.notnot¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ((q ∧ ¬p) ∨ r ∨ ¬s)))
⇒ logic.propositional.genandoveror¬(F ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.genandoveror¬(F ∨ (¬q ∧ q ∧ ¬p) ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.compland¬(F ∨ (F ∧ ¬p) ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.falsezeroand¬(F ∨ F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.falsezeroor¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.genandoveror¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.genandoveror¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s) ∨ (¬r ∧ s ∧ ¬s))
⇒ logic.propositional.compland¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s) ∨ (¬r ∧ F))
⇒ logic.propositional.falsezeroand¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s) ∨ F)
⇒ logic.propositional.falsezeroor¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s))