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, 1, 1, 0, 0, 1, 0, 5, 5, 6, 0, 0, 0, 0, 0, 0, 1, 3, 1, 0]
steps22
major rules3
active labels
  • dnf
  • eliminateimplequiv

enter dnf, check, enter simplify, enter andrules, logic.propositional.truezeroand, exit andrules, exit simplify, check, enter simplify, navigator.down, navigator.down, navigator.right, enter orrules, logic.propositional.falsezeroor, exit orrules, navigator.up, navigator.up, exit simplify, check, enter eliminateimplequiv, navigator.down, logic.propositional.defimpl