Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

(((T /\ ~(p -> q) /\ ~q) || F) /\ T) -> p

⇒ logic.propositional.truezeroand

(((~(p -> q) /\ ~q) || F) /\ T) -> p

⇒ logic.propositional.defimpl

(((~(~p || q) /\ ~q) || F) /\ T) -> p

⇒ logic.propositional.demorganor

(((~~p /\ ~q /\ ~q) || F) /\ T) -> p

⇒ logic.propositional.idempand

(((~~p /\ ~q) || F) /\ T) -> p

⇒ logic.propositional.notnot

(((p /\ ~q) || F) /\ T) -> p