Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

(p /\ (r <-> (p /\ T))) || ((r <-> p) /\ q)

⇒ logic.propositional.defequiv

(p /\ (r <-> (p /\ T))) || (((r /\ p) || (~r /\ ~p)) /\ q)

⇒ logic.propositional.andoveror

(p /\ (r <-> (p /\ T))) || (r /\ p /\ q) || (~r /\ ~p /\ q)