Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(((p || q) /\ r /\ p) || ((p || q) /\ ~r)) /\ (((p || q) /\ r /\ p) || ~p)
⇒ logic.propositional.andoveror((p /\ r /\ p) || (q /\ r /\ p) || ((p || q) /\ ~r)) /\ (((p || q) /\ r /\ p) || ~p)
⇒ logic.propositional.andoveror((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ (((p || q) /\ r /\ p) || ~p)
⇒ logic.propositional.andoveror((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ ((p /\ r /\ p) || (q /\ r /\ p) || ~p)
⇒ logic.propositional.genandoveror(((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ p /\ r /\ p) || (((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ q /\ r /\ p) || (((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ ~p)
⇒ logic.propositional.absorpand(p /\ r /\ p) || (((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ q /\ r /\ p) || (((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ ~p)
⇒ logic.propositional.genandoveror(p /\ r /\ p) || (p /\ r /\ p /\ q /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ ~p)
⇒ logic.propositional.absorpor(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (((p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r) || (q /\ ~r)) /\ ~p)
⇒ logic.propositional.genandoveror(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (p /\ r /\ p /\ ~p) || (q /\ r /\ p /\ ~p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.compland(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (p /\ r /\ F) || (q /\ r /\ p /\ ~p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.compland(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (p /\ r /\ F) || (q /\ r /\ F) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.falsezeroand(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || F || (q /\ r /\ F) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.absorpor(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || F || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.falsezeroor(p /\ r /\ p) || (q /\ r /\ p /\ q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.idempand(p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r /\ q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.absorpor(p /\ r /\ p) || (q /\ r /\ p) || (q /\ ~r /\ q /\ r /\ p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)
⇒ logic.propositional.absorpor(p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)