Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
Final term is not finished¬¬¬(¬(¬(¬q ∨ p) ↔ ((r ↔ s) ∨ ¬s)) ∨ F)
⇒ logic.propositional.demorganor¬¬¬(¬((¬¬q ∧ ¬p) ↔ ((r ↔ s) ∨ ¬s)) ∨ F)
⇒ logic.propositional.falsezeroor¬¬¬¬((¬¬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))