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