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