Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.idempor

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

⇒ logic.propositional.idempor

~p <-> (q /\ p)

⇒ logic.propositional.defequiv

(~p /\ q /\ p) || (~~p /\ ~(q /\ p))

⇒ logic.propositional.notnot

(~p /\ q /\ p) || (p /\ ~(q /\ p))

⇒ logic.propositional.demorganand

(~p /\ q /\ p) || (p /\ (~q || ~p))

⇒ logic.propositional.andoveror

(~p /\ q /\ p) || (p /\ ~q) || (p /\ ~p)

⇒ logic.propositional.compland

(~p /\ q /\ p) || (p /\ ~q) || F

⇒ logic.propositional.falsezeroor

(~p /\ q /\ p) || (p /\ ~q)