Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
Final term is not finishedF ∨ ¬(T ∧ ¬(¬(q → p) ↔ ((r ↔ s) ∨ ¬s)))
⇒ logic.propositional.truezeroandF ∨ ¬¬(¬(q → p) ↔ ((r ↔ s) ∨ ¬s))
⇒ logic.propositional.defimplF ∨ ¬¬(¬(¬q ∨ p) ↔ ((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganorF ∨ ¬¬((¬¬q ∧ ¬p) ↔ ((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnotF ∨ ¬¬((q ∧ ¬p) ↔ ((r ↔ s) ∨ ¬s))
⇒ logic.propositional.defequivF ∨ ¬¬((q ∧ ¬p) ↔ ((r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬s))
⇒ logic.propositional.absorporF ∨ ¬¬((q ∧ ¬p) ↔ ((r ∧ s) ∨ ¬s))
⇒ logic.propositional.oroverandF ∨ ¬¬((q ∧ ¬p) ↔ ((r ∨ ¬s) ∧ (s ∨ ¬s)))
⇒ logic.propositional.complorF ∨ ¬¬((q ∧ ¬p) ↔ ((r ∨ ¬s) ∧ T))
⇒ logic.propositional.truezeroandF ∨ ¬¬((q ∧ ¬p) ↔ (r ∨ ¬s))
⇒ logic.propositional.defequivF ∨ ¬¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ (¬(q ∧ ¬p) ∧ ¬(r ∨ ¬s)))
⇒ logic.propositional.demorganandF ∨ ¬¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ ¬¬p) ∧ ¬(r ∨ ¬s)))
⇒ logic.propositional.notnotF ∨ ¬¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ p) ∧ ¬(r ∨ ¬s)))
⇒ logic.propositional.demorganorF ∨ ¬¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ p) ∧ ¬r ∧ ¬¬s))
⇒ logic.propositional.notnotF ∨ ¬¬((q ∧ ¬p ∧ (r ∨ ¬s)) ∨ ((¬q ∨ p) ∧ ¬r ∧ s))
⇒ logic.propositional.demorganorF ∨ ¬(¬(q ∧ ¬p ∧ (r ∨ ¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s))
⇒ logic.propositional.gendemorganandF ∨ ¬((¬q ∨ ¬¬p ∨ ¬(r ∨ ¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s))
⇒ logic.propositional.notnotF ∨ ¬((¬q ∨ p ∨ ¬(r ∨ ¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s))
⇒ logic.propositional.demorganorF ∨ ¬((¬q ∨ p ∨ (¬r ∧ ¬¬s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s))
⇒ logic.propositional.notnotF ∨ ¬((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬((¬q ∨ p) ∧ ¬r ∧ s))
⇒ logic.propositional.gendemorganandF ∨ ¬((¬q ∨ p ∨ (¬r ∧ s)) ∧ (¬(¬q ∨ p) ∨ ¬¬r ∨ ¬s))
⇒ logic.propositional.notnotF ∨ ¬((¬q ∨ p ∨ (¬r ∧ s)) ∧ (¬(¬q ∨ p) ∨ r ∨ ¬s))
⇒ logic.propositional.demorganorF ∨ ¬((¬q ∨ p ∨ (¬r ∧ s)) ∧ ((¬¬q ∧ ¬p) ∨ r ∨ ¬s))
⇒ logic.propositional.notnotF ∨ ¬((¬q ∨ p ∨ (¬r ∧ s)) ∧ ((q ∧ ¬p) ∨ r ∨ ¬s))
⇒ logic.propositional.genandoverorF ∨ ¬(((¬q ∨ p ∨ (¬r ∧ s)) ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.genandoverorF ∨ ¬((¬q ∧ q ∧ ¬p) ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.complandF ∨ ¬((F ∧ ¬p) ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.falsezeroandF ∨ ¬(F ∨ (p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.falsezeroorF ∨ ¬((p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.genandoverorF ∨ ¬((p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ ((¬q ∨ p ∨ (¬r ∧ s)) ∧ ¬s))
⇒ logic.propositional.genandoverorF ∨ ¬((p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s) ∨ (¬r ∧ s ∧ ¬s))
⇒ logic.propositional.complandF ∨ ¬((p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s) ∨ (¬r ∧ F))
⇒ logic.propositional.falsezeroandF ∨ ¬((p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s) ∨ F)
⇒ logic.propositional.falsezeroorF ∨ ¬((p ∧ q ∧ ¬p) ∨ (¬r ∧ s ∧ q ∧ ¬p) ∨ (¬q ∧ r) ∨ (p ∧ r) ∨ (¬r ∧ s ∧ r) ∨ (¬q ∧ ¬s) ∨ (p ∧ ¬s))