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 || q || (~(p || q) /\ ~p)) /\ p) || ((p || q || (~(p || q) /\ ~p)) /\ ~(p || q) /\ ~p)

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

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

⇒ logic.propositional.genoroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.demorganor

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

⇒ absorpand-subset

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

⇒ absorpand-subset

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