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