Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

Derivation

~q => (p || q) -> p

⇒ logic.propositional.defimpl, initial=TList [TCon logic1.not [TVar "q"]]

~q => ~(p || q) || p

⇒ logic.propositional.demorganor

~q => (~p /\ ~q) || p

⇒ logic.propositional.oroverand

~q => (~p || p) /\ (~q || p)

⇒ logic.propositional.complor

~q => T /\ (~q || p)

⇒ logic.propositional.truezeroand

~q => ~q || p

⇒ commor.sort

~q => p || ~q

⇒ introfalseleft

F || ~q => p || ~q

⇒ introcompl

(p /\ ~p) || ~q => p || ~q

⇒ logic.propositional.oroverand

(p || ~q) /\ (~p || ~q) => p || ~q

⇒ conj-elim

p || ~q => p || ~q