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

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

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

⇒ logic.propositional.genoroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ absorpand-subset

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