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