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