Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(T /\ T /\ ~~p /\ T /\ T /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ ~~(T /\ q) /\ T /\ ~~(T /\ q) /\ ~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(T /\ ~~p /\ T /\ T /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ ~~(T /\ q) /\ T /\ ~~(T /\ q) /\ ~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(T /\ ~~p /\ T /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ ~~(T /\ q) /\ T /\ ~~(T /\ q) /\ ~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(T /\ ~~p /\ T /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ ~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(T /\ ~~p /\ T /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.truezeroand(~~p /\ T /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.truezeroand(~~p /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.notnot(p /\ ~(T /\ ~p) /\ p /\ ~~p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.notnot(p /\ ~(T /\ ~p) /\ p /\ p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(p /\ ~(T /\ ~p) /\ p /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(p /\ ~(T /\ ~p) /\ p /\ ~~~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.notnot(p /\ ~(T /\ ~p) /\ p /\ ~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.idempand(p /\ ~(T /\ ~p)) || (~~(T /\ q) /\ T)
⇒ logic.propositional.truezeroand(p /\ ~~p) || (~~(T /\ q) /\ T)
⇒ logic.propositional.notnot(p /\ p) || (~~(T /\ q) /\ T)
⇒ logic.propositional.idempandp || (~~(T /\ q) /\ T)
⇒ logic.propositional.truezeroandp || ~~(T /\ q)
⇒ logic.propositional.notnotp || (T /\ q)
⇒ logic.propositional.truezeroandp || q