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