Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

Derivation

Final term is not finished

¬(¬((¬(¬q ∨ p) ∨ F) ↔ ((r ↔ (F ∨ s)) ∨ ¬s)) ∨ F)

⇒ logic.propositional.demorganor

¬(¬(((¬¬q ∧ ¬p) ∨ F) ↔ ((r ↔ (F ∨ s)) ∨ ¬s)) ∨ F)

⇒ logic.propositional.falsezeroor

¬(¬((¬¬q ∧ ¬p) ↔ ((r ↔ (F ∨ s)) ∨ ¬s)) ∨ F)

⇒ logic.propositional.notnot

¬(¬((q ∧ ¬p) ↔ ((r ↔ (F ∨ s)) ∨ ¬s)) ∨ F)