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