Exercise logic.propositional.consequence

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

Derivation

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

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

(~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.complor

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

T /\ (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