Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Derivation
p -> q, p -> ~q => ~p
⇒ conj-intro, initial=TList [TCon logic1.implies [TVar "p",TVar "q"],TCon logic1.implies [TVar "p",TCon logic1.not [TVar "q"]]](p -> q) /\ (p -> ~q) => ~p
⇒ logic.propositional.defimpl(~p || q) /\ (p -> ~q) => ~p
⇒ logic.propositional.defimpl(~p || q) /\ (~p || ~q) => ~p
⇒ introfalseleft(~p || q) /\ (~p || ~q) => F || ~p
⇒ introcompl(~p || q) /\ (~p || ~q) => (q /\ ~q) || ~p
⇒ logic.propositional.oroverand(~p || q) /\ (~p || ~q) => (q || ~p) /\ (~q || ~p)
⇒ commor.sort(~p || q) /\ (~p || ~q) => (~p || q) /\ (~q || ~p)
⇒ commor.sort(~p || q) /\ (~p || ~q) => (~p || q) /\ (~p || ~q)