Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Derivation
(~r /\ q) || (~~r /\ ~q) => p -> (q || r)
⇒ logic.propositional.notnot(~r /\ q) || (r /\ ~q) => p -> (q || r)
⇒ logic.propositional.oroverand((~r /\ q) || r) /\ ((~r /\ q) || ~q) => p -> (q || r)
⇒ logic.propositional.oroverand(~r || r) /\ (q || r) /\ ((~r /\ q) || ~q) => p -> (q || r)
⇒ logic.propositional.complorT /\ (q || r) /\ ((~r /\ q) || ~q) => p -> (q || r)
⇒ logic.propositional.oroverandT /\ (q || r) /\ (~r || ~q) /\ (q || ~q) => p -> (q || r)
⇒ logic.propositional.complorT /\ (q || r) /\ (~r || ~q) /\ T => p -> (q || r)
⇒ logic.propositional.truezeroand(q || r) /\ (~r || ~q) /\ T => p -> (q || r)
⇒ logic.propositional.truezeroand(q || r) /\ (~r || ~q) => p -> (q || r)
⇒ logic.propositional.defimpl(q || r) /\ (~r || ~q) => ~p || q || r
⇒ commor.sort(q || r) /\ (~q || ~r) => ~p || q || r
⇒ introfalseleft(F || q || r) /\ (~q || ~r) => ~p || q || r
⇒ introcompl((p /\ ~p) || q || r) /\ (~q || ~r) => ~p || q || r
⇒ logic.propositional.oroverand(p || q || r) /\ (~p || q || r) /\ (~q || ~r) => ~p || q || r
⇒ command-subset(~p || q || r) /\ (p || q || r) /\ (~q || ~r) => ~p || q || r
⇒ conj-elim~p || q || r => ~p || q || r