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)) /\ ~r /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r /\ ~r)) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.idempand~~(((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.notfalse~~(((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.notfalse~~(((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.truezeroand~~(((~~(p /\ ~q) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.notnot~~(((p /\ ~q /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(((p /\ F) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.falsezeroand~~((F || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r)) /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.falsezeroor~~(~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.truezeroand~~(~r /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(~r /\ ~(~F /\ ~(p /\ ~q)) /\ ~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.notfalse~~(~r /\ ~(T /\ ~(p /\ ~q)) /\ ~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.truezeroand~~(~r /\ ~~(p /\ ~q) /\ ~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.notnot~~(~r /\ p /\ ~q /\ ~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.truezeroand~~(~r /\ p /\ ~q /\ ~r /\ ((~~(p /\ ~q) /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.notnot~~(~r /\ p /\ ~q /\ ~r /\ ((p /\ ~q /\ q) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.compland~~(~r /\ p /\ ~q /\ ~r /\ ((p /\ F) || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.falsezeroand~~(~r /\ p /\ ~q /\ ~r /\ (F || (~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))))
⇒ logic.propositional.falsezeroor~~(~r /\ p /\ ~q /\ ~r /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.idempand~~(~r /\ p /\ ~q /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroand~~(~r /\ p /\ ~q /\ ~r /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.compland~~(~r /\ p /\ ~q /\ ~r /\ ~(~F /\ ~(p /\ ~q)))
⇒ logic.propositional.notfalse~~(~r /\ p /\ ~q /\ ~r /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroand~~(~r /\ p /\ ~q /\ ~r /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(~r /\ p /\ ~q /\ ~r /\ p /\ ~q)
⇒ logic.propositional.idempand~~(~r /\ p /\ ~q)