Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished~~(((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~r /\ ~r /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~r /\ ~r /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ ~r /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.idempand~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.idempand~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.idempand~~((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q))))
⇒ logic.propositional.notfalse~~((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q))))
⇒ logic.propositional.truezeroand~~((~~(p /\ ~q) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q))))
⇒ logic.propositional.notnot~~((p /\ ~q /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q))))
⇒ logic.propositional.compland~~((p /\ F) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q))))
⇒ logic.propositional.falsezeroand~~(F || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q))))
⇒ logic.propositional.falsezeroor~~(~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroand~~(~r /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.compland~~(~r /\ ~(~F /\ ~(p /\ ~q)))
⇒ logic.propositional.notfalse~~(~r /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroand~~(~r /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(~r /\ p /\ ~q)