Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

¬(¬q ∨ p) ↔ ((r ↔ s) ∨ ¬s)
ready: no

Feedback

Path 1

path[0, 1, 0, 4, 0, 1, 3, 0]
steps8
major rules2
active labels
  • dnf
  • eliminateimplequiv

enter dnf, check, enter simplify, logic.propositional.notnot, exit simplify, check, enter eliminateimplequiv, logic.propositional.defimpl