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 [TVar "q"]

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.genoroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ 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