Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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