Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.nottrue

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

⇒ logic.propositional.falsezeroor

T /\ ((p /\ T) || q)

⇒ logic.propositional.truezeroand

T /\ (p || q)