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