Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
T /\ ((~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r /\ ~r))
⇒ logic.propositional.truezeroand(~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r /\ ~r)
⇒ logic.propositional.idempand(~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.truezeroand(~~(~~(~q /\ (q || p)) /\ T) /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.notnot(~~(~q /\ (q || p)) /\ T /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.truezeroand(~~(~q /\ (q || p)) /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.notnot(~q /\ (q || p) /\ ~~q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.notnot(~q /\ (q || p) /\ q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.absorpand(~q /\ q) || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.complandF || (~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r)
⇒ logic.propositional.falsezeroor~~(~~(~q /\ (q || p)) /\ T) /\ T /\ ~r
⇒ logic.propositional.truezeroand~~(~~(~q /\ (q || p)) /\ T) /\ ~r
⇒ logic.propositional.notnot~~(~q /\ (q || p)) /\ T /\ ~r
⇒ logic.propositional.truezeroand~~(~q /\ (q || p)) /\ ~r
⇒ logic.propositional.notnot~q /\ (q || p) /\ ~r
⇒ logic.propositional.andoveror((~q /\ q) || (~q /\ p)) /\ ~r
⇒ logic.propositional.compland(F || (~q /\ p)) /\ ~r
⇒ logic.propositional.falsezeroor~q /\ p /\ ~r