Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Derivation
p -> (q /\ r) => (p /\ q) <-> (p /\ r)
⇒ logic.propositional.defimpl, initial=TList [TCon logic1.implies [TVar "p",TCon logic1.and [TVar "q",TVar "r"]]]~p || (q /\ r) => (p /\ q) <-> (p /\ r)
⇒ logic.propositional.oroverand(~p || q) /\ (~p || r) => (p /\ q) <-> (p /\ r)
⇒ logic.propositional.defequiv(~p || q) /\ (~p || r) => (p /\ q /\ p /\ r) || (~(p /\ q) /\ ~(p /\ r))
⇒ logic.propositional.demorganand(~p || q) /\ (~p || r) => (p /\ q /\ p /\ r) || ((~p || ~q) /\ ~(p /\ r))
⇒ logic.propositional.demorganand(~p || q) /\ (~p || r) => (p /\ q /\ p /\ r) || ((~p || ~q) /\ (~p || ~r))
⇒ logic.propositional.genoroverand(~p || q) /\ (~p || r) => (p || ((~p || ~q) /\ (~p || ~r))) /\ (q || ((~p || ~q) /\ (~p || ~r))) /\ (p || ((~p || ~q) /\ (~p || ~r))) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.oroverand(~p || q) /\ (~p || r) => (p || ~p || ~q) /\ (p || ~p || ~r) /\ (q || ((~p || ~q) /\ (~p || ~r))) /\ (p || ((~p || ~q) /\ (~p || ~r))) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.complor(~p || q) /\ (~p || r) => (T || ~q) /\ (p || ~p || ~r) /\ (q || ((~p || ~q) /\ (~p || ~r))) /\ (p || ((~p || ~q) /\ (~p || ~r))) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.complor(~p || q) /\ (~p || r) => (T || ~q) /\ (T || ~r) /\ (q || ((~p || ~q) /\ (~p || ~r))) /\ (p || ((~p || ~q) /\ (~p || ~r))) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.oroverand(~p || q) /\ (~p || r) => (T || ~q) /\ (T || ~r) /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (p || ((~p || ~q) /\ (~p || ~r))) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.oroverand(~p || q) /\ (~p || r) => (T || ~q) /\ (T || ~r) /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (p || ~p || ~q) /\ (p || ~p || ~r) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.complor(~p || q) /\ (~p || r) => (T || ~q) /\ (T || ~r) /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (T || ~q) /\ (p || ~p || ~r) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.complor(~p || q) /\ (~p || r) => (T || ~q) /\ (T || ~r) /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (T || ~q) /\ (T || ~r) /\ (r || ((~p || ~q) /\ (~p || ~r)))
⇒ logic.propositional.oroverand(~p || q) /\ (~p || r) => (T || ~q) /\ (T || ~r) /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (T || ~q) /\ (T || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.truezeroor(~p || q) /\ (~p || r) => T /\ (T || ~r) /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (T || ~q) /\ (T || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.absorpand(~p || q) /\ (~p || r) => T /\ (q || ~p || ~q) /\ (q || ~p || ~r) /\ (T || ~q) /\ (T || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.truezeroand(~p || q) /\ (~p || r) => (q || ~p || ~q) /\ (q || ~p || ~r) /\ (T || ~q) /\ (T || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.truezeroor(~p || q) /\ (~p || r) => (q || ~p || ~q) /\ (q || ~p || ~r) /\ T /\ (T || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.absorpand(~p || q) /\ (~p || r) => (q || ~p || ~q) /\ (q || ~p || ~r) /\ T /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.truezeroand(~p || q) /\ (~p || r) => (q || ~p || ~q) /\ (q || ~p || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ commor.sort(~p || q) /\ (~p || r) => (~p || q || ~q) /\ (q || ~p || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.complor(~p || q) /\ (~p || r) => (~p || T) /\ (q || ~p || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.truezeroor(~p || q) /\ (~p || r) => T /\ (q || ~p || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ logic.propositional.truezeroand(~p || q) /\ (~p || r) => (q || ~p || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ commor.sort(~p || q) /\ (~p || r) => (~p || q || ~r) /\ (r || ~p || ~q) /\ (r || ~p || ~r)
⇒ commor.sort(~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r) /\ (r || ~p || ~r)
⇒ commor.sort(~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r) /\ (~p || r || ~r)
⇒ logic.propositional.complor(~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r) /\ (~p || T)
⇒ logic.propositional.truezeroor(~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r) /\ T
⇒ logic.propositional.truezeroand(~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ introfalseleft(F || ~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ introcompl((r /\ ~r) || ~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ logic.propositional.oroverand(r || ~p || q) /\ (~r || ~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ commor.sort(~p || q || r) /\ (~r || ~p || q) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ commor.sort(~p || q || r) /\ (~p || q || ~r) /\ (~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ introfalseleft(~p || q || r) /\ (~p || q || ~r) /\ (F || ~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ introcompl(~p || q || r) /\ (~p || q || ~r) /\ ((q /\ ~q) || ~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ logic.propositional.oroverand(~p || q || r) /\ (~p || q || ~r) /\ (q || ~p || r) /\ (~q || ~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ commor.sort(~p || q || r) /\ (~p || q || ~r) /\ (~p || q || r) /\ (~q || ~p || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ commor.sort(~p || q || r) /\ (~p || q || ~r) /\ (~p || q || r) /\ (~p || ~q || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ command-subset(~p || q || ~r) /\ (~p || ~q || r) /\ (~p || q || r) /\ (~p || q || r) => (~p || q || ~r) /\ (~p || ~q || r)
⇒ conj-elim(~p || q || ~r) /\ (~p || ~q || r) => (~p || q || ~r) /\ (~p || ~q || r)