Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
(¬(p ∨ ¬q) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(¬p ∧ ¬¬q ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(¬p ∧ q ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.defequiv(¬p ∧ q ∧ ((r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.absorpor(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (¬¬(p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ↔ s) ∧ ¬¬s)
⇒ logic.propositional.notnot(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ↔ s) ∧ s)
⇒ logic.propositional.defequiv(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ s)
⇒ logic.propositional.demorganor(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ∧ s) ∧ ¬(¬r ∧ ¬s) ∧ s)
⇒ logic.propositional.demorganand(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ∧ s) ∧ (¬¬r ∨ ¬¬s) ∧ s)
⇒ logic.propositional.notnot(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ∧ s) ∧ (r ∨ ¬¬s) ∧ s)
⇒ logic.propositional.notnot(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ∧ s) ∧ (r ∨ s) ∧ s)
⇒ logic.propositional.absorpand(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ ¬(r ∧ s) ∧ s)
⇒ logic.propositional.demorganand(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((p ∨ ¬q) ∧ (¬r ∨ ¬s) ∧ s)
⇒ logic.propositional.andoveror(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ ((((p ∨ ¬q) ∧ ¬r) ∨ ((p ∨ ¬q) ∧ ¬s)) ∧ s)
⇒ logic.propositional.andoveror(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (((p ∧ ¬r) ∨ (¬q ∧ ¬r) ∨ ((p ∨ ¬q) ∧ ¬s)) ∧ s)
⇒ logic.propositional.andoveror(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (((p ∧ ¬r) ∨ (¬q ∧ ¬r) ∨ (p ∧ ¬s) ∨ (¬q ∧ ¬s)) ∧ s)
⇒ logic.propositional.genandoveror(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s) ∨ (p ∧ ¬s ∧ s) ∨ (¬q ∧ ¬s ∧ s)
⇒ logic.propositional.compland(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s) ∨ (p ∧ F) ∨ (¬q ∧ ¬s ∧ s)
⇒ logic.propositional.compland(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s) ∨ (p ∧ F) ∨ (¬q ∧ F)
⇒ logic.propositional.falsezeroand(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s) ∨ F ∨ (¬q ∧ F)
⇒ logic.propositional.absorpor(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s) ∨ F
⇒ logic.propositional.falsezeroor(¬p ∧ q ∧ ((r ∧ s) ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s)
⇒ logic.propositional.oroverand(¬p ∧ q ∧ (r ∨ ¬s) ∧ (s ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s)
⇒ logic.propositional.complor(¬p ∧ q ∧ (r ∨ ¬s) ∧ T) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s)
⇒ logic.propositional.truezeroand(¬p ∧ q ∧ (r ∨ ¬s)) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s)
⇒ logic.propositional.andoveror(¬p ∧ ((q ∧ r) ∨ (q ∧ ¬s))) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s)
⇒ logic.propositional.andoveror(¬p ∧ q ∧ r) ∨ (¬p ∧ q ∧ ¬s) ∨ (p ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s)