Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished~(~T || ~T) /\ p /\ ~q /\ ~(~((F || T) /\ T) || ~~~~~(p /\ ~q) || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~F /\ ~q))
⇒ logic.propositional.absorpand~(~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.notnot~(~T || ~T) /\ p /\ ~q /\ ~(~T || ~~~(p /\ ~q) || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.notnot~(~T || ~T) /\ p /\ ~q /\ ~(~T || ~(p /\ ~q) || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.demorganand~(~T || ~T) /\ p /\ ~q /\ ~(~T || ~p || ~~q || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.notnot~(~T || ~T) /\ p /\ ~q /\ ~(~T || ~p || q || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.nottrue~(~T || ~T) /\ p /\ ~q /\ ~(F || ~p || q || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.falsezeroor~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(T /\ ((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.truezeroand~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~F /\ ~q))
⇒ logic.propositional.notfalse~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ T /\ ~q))
⇒ logic.propositional.truezeroand~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(((T /\ q) || ~r) /\ p /\ ~~(p /\ ~q) /\ ~q))
⇒ logic.propositional.notnot~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(((T /\ q) || ~r) /\ p /\ p /\ ~q /\ ~q))
⇒ logic.propositional.idempand~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(((T /\ q) || ~r) /\ p /\ p /\ ~q))
⇒ logic.propositional.idempand~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(((T /\ q) || ~r) /\ p /\ ~q))
⇒ logic.propositional.truezeroand~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~((q || ~r) /\ p /\ ~q))
⇒ logic.propositional.gendemorganand~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || ~(q || ~r) || ~p || ~~q)
⇒ logic.propositional.demorganor~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || (~q /\ ~~r) || ~p || ~~q)
⇒ logic.propositional.notnot~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || (~q /\ r) || ~p || ~~q)
⇒ logic.propositional.notnot~(~T || ~T) /\ p /\ ~q /\ ~(~p || q || (~q /\ r) || ~p || q)