Exercise logic.propositional.consequence

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

Derivation

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

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

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

~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