Exercise logic.propositional.consequence

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

Derivation

Final term is not finished

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

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

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

⇒ logic.propositional.genoroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.idempand

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