Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (T /\ (F || T) /\ ~~~~p /\ ~(p /\ q))) /\ T
⇒ logic.propositional.absorpand((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (T /\ ~~~~p /\ ~(p /\ q))) /\ T
⇒ logic.propositional.truezeroand((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (~~~~p /\ ~(p /\ q))) /\ T
⇒ logic.propositional.notnot((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (~~p /\ ~(p /\ q))) /\ T
⇒ logic.propositional.notnot((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (p /\ ~(p /\ q))) /\ T
⇒ logic.propositional.demorganand((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (p /\ (~p || ~q))) /\ T
⇒ logic.propositional.andoveror((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (p /\ ~p) || (p /\ ~q)) /\ T
⇒ logic.propositional.compland((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || F || (p /\ ~q)) /\ T
⇒ logic.propositional.falsezeroor((~(~~p /\ ~~p) /\ ~~(p /\ T /\ q)) || (p /\ ~q)) /\ T