Exercise logic.propositional.proof.unicode
Description
Prove two propositions equivalent (unicode support)
Derivations
1.
¬(p ∧ q) ∨ s ∨ ¬r == (p ∧ q) → (r → s)
⇒ logic.propositional.defimpl¬(p ∧ q) ∨ s ∨ ¬r == ¬(p ∧ q) ∨ (r → s)
⇒ logic.propositional.defimpl¬(p ∧ q) ∨ s ∨ ¬r == ¬(p ∧ q) ∨ ¬r ∨ s
⇒ top-is-or.com¬(p ∧ q) ∨ s ∨ ¬r == ¬(p ∧ q) ∨ s ∨ ¬r
2.
¬((p → q) → (p ∧ q)) == (p → q) ∧ (¬p ∨ ¬q)
⇒ logic.propositional.defimpl¬(¬(p → q) ∨ (p ∧ q)) == (p → q) ∧ (¬p ∨ ¬q)
⇒ logic.propositional.demorganor¬¬(p → q) ∧ ¬(p ∧ q) == (p → q) ∧ (¬p ∨ ¬q)
⇒ logic.propositional.notnot(p → q) ∧ ¬(p ∧ q) == (p → q) ∧ (¬p ∨ ¬q)
⇒ logic.propositional.demorganand(p → q) ∧ (¬p ∨ ¬q) == (p → q) ∧ (¬p ∨ ¬q)
3.
¬((p ↔ q) → (p ∨ (p ↔ q))) == F
⇒ logic.propositional.defimpl¬(¬(p ↔ q) ∨ p ∨ (p ↔ q)) == F
⇒ complor.sort¬(¬(p ↔ q) ∨ (p ↔ q) ∨ p) == F
⇒ logic.propositional.complor¬(T ∨ p) == F
⇒ logic.propositional.truezeroor¬T == F
⇒ logic.propositional.nottrueF == F
4.
(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∨ q) ∧ ¬(p ∧ q)
⇒ logic.propositional.demorganand(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∨ q) ∧ (¬p ∨ ¬q)
⇒ logic.propositional.andoveror(p ∧ ¬q) ∨ (q ∧ ¬p) == ((p ∨ q) ∧ ¬p) ∨ ((p ∨ q) ∧ ¬q)
⇒ top-is-or.com(p ∧ ¬q) ∨ (q ∧ ¬p) == ((p ∨ q) ∧ ¬q) ∨ ((p ∨ q) ∧ ¬p)
⇒ logic.propositional.andoveror(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∧ ¬q) ∨ (q ∧ ¬q) ∨ ((p ∨ q) ∧ ¬p)
⇒ logic.propositional.compland(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∧ ¬q) ∨ F ∨ ((p ∨ q) ∧ ¬p)
⇒ logic.propositional.falsezeroor(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∧ ¬q) ∨ ((p ∨ q) ∧ ¬p)
⇒ logic.propositional.andoveror(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∧ ¬q) ∨ (p ∧ ¬p) ∨ (q ∧ ¬p)
⇒ logic.propositional.compland(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∧ ¬q) ∨ F ∨ (q ∧ ¬p)
⇒ logic.propositional.falsezeroor(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∧ ¬q) ∨ (q ∧ ¬p)
5.
(p ∧ q ∧ r) ∨ (¬p ∧ q) == (¬p ∧ q ∧ ¬r) ∨ (q ∧ r)
⇒ command.common-literal(q ∧ p ∧ r) ∨ (q ∧ ¬p) == (¬p ∧ q ∧ ¬r) ∨ (q ∧ r)
⇒ command.common-literal(q ∧ p ∧ r) ∨ (q ∧ ¬p) == (q ∧ ¬p ∧ ¬r) ∨ (q ∧ r)
⇒ andoveror.inv.common-literalq ∧ ((p ∧ r) ∨ ¬p) == (q ∧ ¬p ∧ ¬r) ∨ (q ∧ r)
⇒ andoveror.inv.common-literalq ∧ ((p ∧ r) ∨ ¬p) == q ∧ ((¬p ∧ ¬r) ∨ r)
⇒ logic.propositional.oroverandq ∧ (p ∨ ¬p) ∧ (r ∨ ¬p) == q ∧ ((¬p ∧ ¬r) ∨ r)
⇒ logic.propositional.complorq ∧ T ∧ (r ∨ ¬p) == q ∧ ((¬p ∧ ¬r) ∨ r)
⇒ logic.propositional.truezeroandq ∧ (r ∨ ¬p) == q ∧ ((¬p ∧ ¬r) ∨ r)
⇒ logic.propositional.oroverandq ∧ (r ∨ ¬p) == q ∧ (¬p ∨ r) ∧ (¬r ∨ r)
⇒ logic.propositional.complorq ∧ (r ∨ ¬p) == q ∧ (¬p ∨ r) ∧ T
⇒ logic.propositional.truezeroandq ∧ (r ∨ ¬p) == q ∧ (¬p ∨ r)
⇒ top-is-or.comq ∧ (r ∨ ¬p) == q ∧ (r ∨ ¬p)
6.
¬(p ∨ ¬(p ∨ ¬q)) == ¬(p ∨ q)
⇒ logic.propositional.demorganor¬(p ∨ (¬p ∧ ¬¬q)) == ¬(p ∨ q)
⇒ logic.propositional.notnot¬(p ∨ (¬p ∧ q)) == ¬(p ∨ q)
⇒ logic.propositional.oroverand¬((p ∨ ¬p) ∧ (p ∨ q)) == ¬(p ∨ q)
⇒ logic.propositional.complor¬(T ∧ (p ∨ q)) == ¬(p ∨ q)
⇒ logic.propositional.truezeroand¬(p ∨ q) == ¬(p ∨ q)
7.
(p ∧ q) → p == T
⇒ logic.propositional.defimpl¬(p ∧ q) ∨ p == T
⇒ logic.propositional.demorganand¬p ∨ ¬q ∨ p == T
⇒ complor.sort¬p ∨ p ∨ ¬q == T
⇒ logic.propositional.complorT ∨ ¬q == T
⇒ logic.propositional.truezeroorT == T
8.
(p → q) → (p → s) == (¬q → ¬p) → (¬s → ¬p)
⇒ logic.propositional.defimpl(¬p ∨ q) → (p → s) == (¬q → ¬p) → (¬s → ¬p)
⇒ logic.propositional.defimpl(¬p ∨ q) → (p → s) == (¬¬q ∨ ¬p) → (¬s → ¬p)
⇒ top-is-or.com(¬p ∨ q) → (p → s) == (¬p ∨ ¬¬q) → (¬s → ¬p)
⇒ logic.propositional.notnot(¬p ∨ q) → (p → s) == (¬p ∨ q) → (¬s → ¬p)
⇒ logic.propositional.defimpl(¬p ∨ q) → (¬p ∨ s) == (¬p ∨ q) → (¬s → ¬p)
⇒ logic.propositional.defimpl(¬p ∨ q) → (¬p ∨ s) == (¬p ∨ q) → (¬¬s ∨ ¬p)
⇒ top-is-or.com(¬p ∨ q) → (¬p ∨ s) == (¬p ∨ q) → (¬p ∨ ¬¬s)
⇒ logic.propositional.notnot(¬p ∨ q) → (¬p ∨ s) == (¬p ∨ q) → (¬p ∨ s)
9.
p ∧ q == ¬(p → ¬q)
⇒ logic.propositional.defimplp ∧ q == ¬(¬p ∨ ¬q)
⇒ logic.propositional.demorganorp ∧ q == ¬¬p ∧ ¬¬q
⇒ logic.propositional.notnotp ∧ q == p ∧ ¬¬q
⇒ logic.propositional.notnotp ∧ q == p ∧ q
10.
¬(p ∨ (¬p ∧ q)) == ¬(p ∨ q)
⇒ logic.propositional.oroverand¬((p ∨ ¬p) ∧ (p ∨ q)) == ¬(p ∨ q)
⇒ logic.propositional.complor¬(T ∧ (p ∨ q)) == ¬(p ∨ q)
⇒ logic.propositional.truezeroand¬(p ∨ q) == ¬(p ∨ q)
11.
(p → q) ∨ ¬p == (p → q) ∨ q
⇒ logic.propositional.defimpl¬p ∨ q ∨ ¬p == (p → q) ∨ q
⇒ complor.sort¬p ∨ ¬p ∨ q == (p → q) ∨ q
⇒ logic.propositional.idempor¬p ∨ q == (p → q) ∨ q
⇒ logic.propositional.defimpl¬p ∨ q == ¬p ∨ q ∨ q
⇒ logic.propositional.idempor¬p ∨ q == ¬p ∨ q
12.
p ↔ q == (p → q) ∧ (q → p)
⇒ logic.propositional.defimplp ↔ q == (¬p ∨ q) ∧ (q → p)
⇒ logic.propositional.defimplp ↔ q == (¬p ∨ q) ∧ (¬q ∨ p)
⇒ logic.propositional.defequiv(p ∧ q) ∨ (¬p ∧ ¬q) == (¬p ∨ q) ∧ (¬q ∨ p)
⇒ logic.propositional.andoveror(p ∧ q) ∨ (¬p ∧ ¬q) == ((¬p ∨ q) ∧ ¬q) ∨ ((¬p ∨ q) ∧ p)
⇒ top-is-or.com(p ∧ q) ∨ (¬p ∧ ¬q) == ((¬p ∨ q) ∧ p) ∨ ((¬p ∨ q) ∧ ¬q)
⇒ logic.propositional.andoveror(p ∧ q) ∨ (¬p ∧ ¬q) == (¬p ∧ p) ∨ (q ∧ p) ∨ ((¬p ∨ q) ∧ ¬q)
⇒ logic.propositional.compland(p ∧ q) ∨ (¬p ∧ ¬q) == F ∨ (q ∧ p) ∨ ((¬p ∨ q) ∧ ¬q)
⇒ logic.propositional.falsezeroor(p ∧ q) ∨ (¬p ∧ ¬q) == (q ∧ p) ∨ ((¬p ∨ q) ∧ ¬q)
⇒ top-is-and.com(p ∧ q) ∨ (¬p ∧ ¬q) == (p ∧ q) ∨ ((¬p ∨ q) ∧ ¬q)
⇒ logic.propositional.andoveror(p ∧ q) ∨ (¬p ∧ ¬q) == (p ∧ q) ∨ (¬p ∧ ¬q) ∨ (q ∧ ¬q)
⇒ logic.propositional.compland(p ∧ q) ∨ (¬p ∧ ¬q) == (p ∧ q) ∨ (¬p ∧ ¬q) ∨ F
⇒ logic.propositional.falsezeroor(p ∧ q) ∨ (¬p ∧ ¬q) == (p ∧ q) ∨ (¬p ∧ ¬q)
13.
(p → q) ∨ (q → p) == T
⇒ logic.propositional.defimpl¬p ∨ q ∨ (q → p) == T
⇒ logic.propositional.defimpl¬p ∨ q ∨ ¬q ∨ p == T
⇒ logic.propositional.complor¬p ∨ T ∨ p == T
⇒ logic.propositional.truezeroor¬p ∨ T == T
⇒ logic.propositional.truezeroorT == T
14.
(q → (¬p → q)) → p == ¬p → (q ∧ p ∧ q ∧ q)
⇒ logic.propositional.idempand(q → (¬p → q)) → p == ¬p → (q ∧ p ∧ q)
⇒ compland.sort(q → (¬p → q)) → p == ¬p → (q ∧ q ∧ p)
⇒ logic.propositional.idempand(q → (¬p → q)) → p == ¬p → (q ∧ p)
⇒ logic.propositional.defimpl¬(q → (¬p → q)) ∨ p == ¬p → (q ∧ p)
⇒ logic.propositional.defimpl¬(¬q ∨ (¬p → q)) ∨ p == ¬p → (q ∧ p)
⇒ logic.propositional.demorganor(¬¬q ∧ ¬(¬p → q)) ∨ p == ¬p → (q ∧ p)
⇒ logic.propositional.notnot(q ∧ ¬(¬p → q)) ∨ p == ¬p → (q ∧ p)
⇒ logic.propositional.defimpl(q ∧ ¬(¬¬p ∨ q)) ∨ p == ¬p → (q ∧ p)
⇒ logic.propositional.notnot(q ∧ ¬(p ∨ q)) ∨ p == ¬p → (q ∧ p)
⇒ logic.propositional.defimpl(q ∧ ¬(p ∨ q)) ∨ p == ¬¬p ∨ (q ∧ p)
⇒ logic.propositional.notnot(q ∧ ¬(p ∨ q)) ∨ p == p ∨ (q ∧ p)
⇒ logic.propositional.absorpor(q ∧ ¬(p ∨ q)) ∨ p == p
⇒ logic.propositional.demorganor(q ∧ ¬p ∧ ¬q) ∨ p == p
⇒ compland.sort(q ∧ ¬q ∧ ¬p) ∨ p == p
⇒ logic.propositional.compland(F ∧ ¬p) ∨ p == p
⇒ logic.propositional.falsezeroandF ∨ p == p
⇒ logic.propositional.falsezeroorp == p
15.
(p → ¬q) → q == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.defimpl¬(p → ¬q) ∨ q == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.defimpl¬(¬p ∨ ¬q) ∨ q == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.demorganor(¬¬p ∧ ¬¬q) ∨ q == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.notnot(p ∧ ¬¬q) ∨ q == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.notnot(p ∧ q) ∨ q == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.absorporq == (s ∨ (s → (q ∨ p))) ∧ q
⇒ logic.propositional.defimplq == (s ∨ ¬s ∨ q ∨ p) ∧ q
⇒ logic.propositional.complorq == (T ∨ q ∨ p) ∧ q
⇒ logic.propositional.truezeroorq == T ∧ q
⇒ logic.propositional.truezeroandq == q
16.
p → (q → r) == (p → q) → (p → r)
⇒ logic.propositional.defimpl¬p ∨ (q → r) == (p → q) → (p → r)
⇒ logic.propositional.defimpl¬p ∨ ¬q ∨ r == (p → q) → (p → r)
⇒ logic.propositional.defimpl¬p ∨ ¬q ∨ r == ¬(p → q) ∨ (p → r)
⇒ logic.propositional.defimpl¬p ∨ ¬q ∨ r == ¬(¬p ∨ q) ∨ (p → r)
⇒ logic.propositional.demorganor¬p ∨ ¬q ∨ r == (¬¬p ∧ ¬q) ∨ (p → r)
⇒ logic.propositional.notnot¬p ∨ ¬q ∨ r == (p ∧ ¬q) ∨ (p → r)
⇒ logic.propositional.defimpl¬p ∨ ¬q ∨ r == (p ∧ ¬q) ∨ ¬p ∨ r
⇒ logic.propositional.oroverand¬p ∨ ¬q ∨ r == ((p ∨ ¬p) ∧ (¬q ∨ ¬p)) ∨ r
⇒ logic.propositional.complor¬p ∨ ¬q ∨ r == (T ∧ (¬q ∨ ¬p)) ∨ r
⇒ logic.propositional.truezeroand¬p ∨ ¬q ∨ r == ¬q ∨ ¬p ∨ r
⇒ top-is-or.com¬p ∨ ¬q ∨ r == ¬p ∨ ¬q ∨ r
17.
¬((p → q) → ¬(q → p)) == p ↔ q
⇒ logic.propositional.defimpl¬(¬(p → q) ∨ ¬(q → p)) == p ↔ q
⇒ logic.propositional.demorganor¬¬(p → q) ∧ ¬¬(q → p) == p ↔ q
⇒ logic.propositional.notnot(p → q) ∧ ¬¬(q → p) == p ↔ q
⇒ logic.propositional.notnot(p → q) ∧ (q → p) == p ↔ q
⇒ logic.propositional.defimpl(¬p ∨ q) ∧ (q → p) == p ↔ q
⇒ logic.propositional.defimpl(¬p ∨ q) ∧ (¬q ∨ p) == p ↔ q
⇒ logic.propositional.defequiv(¬p ∨ q) ∧ (¬q ∨ p) == (p ∧ q) ∨ (¬p ∧ ¬q)
⇒ logic.propositional.andoveror((¬p ∨ q) ∧ ¬q) ∨ ((¬p ∨ q) ∧ p) == (p ∧ q) ∨ (¬p ∧ ¬q)
⇒ top-is-or.com((¬p ∨ q) ∧ ¬q) ∨ ((¬p ∨ q) ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ logic.propositional.andoveror(¬p ∧ ¬q) ∨ (q ∧ ¬q) ∨ ((¬p ∨ q) ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ logic.propositional.compland(¬p ∧ ¬q) ∨ F ∨ ((¬p ∨ q) ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ logic.propositional.falsezeroor(¬p ∧ ¬q) ∨ ((¬p ∨ q) ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ logic.propositional.andoveror(¬p ∧ ¬q) ∨ (¬p ∧ p) ∨ (q ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ logic.propositional.compland(¬p ∧ ¬q) ∨ F ∨ (q ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ logic.propositional.falsezeroor(¬p ∧ ¬q) ∨ (q ∧ p) == (¬p ∧ ¬q) ∨ (p ∧ q)
⇒ top-is-and.com(¬p ∧ ¬q) ∨ (q ∧ p) == (¬p ∧ ¬q) ∨ (q ∧ p)
18.
19.
¬(¬p ∧ ¬(q ∨ r)) == p ∨ q ∨ r
⇒ logic.propositional.demorganand¬¬p ∨ ¬¬(q ∨ r) == p ∨ q ∨ r
⇒ logic.propositional.notnotp ∨ ¬¬(q ∨ r) == p ∨ q ∨ r
⇒ logic.propositional.notnotp ∨ q ∨ r == p ∨ q ∨ r
20.
¬(p ∧ (q ∨ r)) == ¬p ∨ (¬q ∧ ¬r)
⇒ logic.propositional.demorganand¬p ∨ ¬(q ∨ r) == ¬p ∨ (¬q ∧ ¬r)
⇒ logic.propositional.demorganor¬p ∨ (¬q ∧ ¬r) == ¬p ∨ (¬q ∧ ¬r)
21.
p ↔ (q ↔ p) == q
⇒ logic.propositional.defequivp ↔ ((q ∧ p) ∨ (¬q ∧ ¬p)) == q
⇒ logic.propositional.defequiv(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ ¬((q ∧ p) ∨ (¬q ∧ ¬p))) == q
⇒ logic.propositional.demorganor(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ ¬(q ∧ p) ∧ ¬(¬q ∧ ¬p)) == q
⇒ logic.propositional.demorganand(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ ¬(q ∧ p) ∧ (¬¬q ∨ ¬¬p)) == q
⇒ logic.propositional.notnot(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ ¬(q ∧ p) ∧ (q ∨ ¬¬p)) == q
⇒ logic.propositional.notnot(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ ¬(q ∧ p) ∧ (q ∨ p)) == q
⇒ logic.propositional.demorganand(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ (¬q ∨ ¬p) ∧ (q ∨ p)) == q
⇒ logic.propositional.absorpand(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ (q ∨ p)) == q
⇒ logic.propositional.andoveror(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ q) ∨ (¬p ∧ p) == q
⇒ logic.propositional.compland(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ q) ∨ F == q
⇒ logic.propositional.falsezeroor(p ∧ ((q ∧ p) ∨ (¬q ∧ ¬p))) ∨ (¬p ∧ q) == q
⇒ logic.propositional.andoveror(p ∧ q ∧ p) ∨ (p ∧ ¬q ∧ ¬p) ∨ (¬p ∧ q) == q
⇒ compland.sort(p ∧ p ∧ q) ∨ (p ∧ ¬q ∧ ¬p) ∨ (¬p ∧ q) == q
⇒ logic.propositional.idempand(p ∧ q) ∨ (p ∧ ¬q ∧ ¬p) ∨ (¬p ∧ q) == q
⇒ compland.sort(p ∧ q) ∨ (p ∧ ¬p ∧ ¬q) ∨ (¬p ∧ q) == q
⇒ logic.propositional.compland(p ∧ q) ∨ (F ∧ ¬q) ∨ (¬p ∧ q) == q
⇒ logic.propositional.falsezeroand(p ∧ q) ∨ F ∨ (¬p ∧ q) == q
⇒ logic.propositional.falsezeroor(p ∧ q) ∨ (¬p ∧ q) == q
⇒ andoveror.inv.common-literal(p ∨ ¬p) ∧ q == q
⇒ logic.propositional.complorT ∧ q == q
⇒ logic.propositional.truezeroandq == q
22.
(p → q) → ¬p == p → (q → ¬p)
⇒ logic.propositional.defimpl¬(p → q) ∨ ¬p == p → (q → ¬p)
⇒ logic.propositional.defimpl¬(¬p ∨ q) ∨ ¬p == p → (q → ¬p)
⇒ logic.propositional.demorganor(¬¬p ∧ ¬q) ∨ ¬p == p → (q → ¬p)
⇒ logic.propositional.notnot(p ∧ ¬q) ∨ ¬p == p → (q → ¬p)
⇒ logic.propositional.oroverand(p ∨ ¬p) ∧ (¬q ∨ ¬p) == p → (q → ¬p)
⇒ logic.propositional.complorT ∧ (¬q ∨ ¬p) == p → (q → ¬p)
⇒ logic.propositional.truezeroand¬q ∨ ¬p == p → (q → ¬p)
⇒ logic.propositional.defimpl¬q ∨ ¬p == ¬p ∨ (q → ¬p)
⇒ logic.propositional.defimpl¬q ∨ ¬p == ¬p ∨ ¬q ∨ ¬p
⇒ top-is-or.com¬q ∨ ¬p == ¬q ∨ ¬p ∨ ¬p
⇒ logic.propositional.idempor¬q ∨ ¬p == ¬q ∨ ¬p
23.
(¬q ∧ p) → p == (¬q ↔ q) → p
⇒ logic.propositional.defimpl¬(¬q ∧ p) ∨ p == (¬q ↔ q) → p
⇒ logic.propositional.demorganand¬¬q ∨ ¬p ∨ p == (¬q ↔ q) → p
⇒ logic.propositional.complor¬¬q ∨ T == (¬q ↔ q) → p
⇒ logic.propositional.truezeroorT == (¬q ↔ q) → p
⇒ logic.propositional.defimplT == ¬(¬q ↔ q) ∨ p
⇒ logic.propositional.defequivT == ¬((¬q ∧ q) ∨ (¬¬q ∧ ¬q)) ∨ p
⇒ logic.propositional.complandT == ¬(F ∨ (¬¬q ∧ ¬q)) ∨ p
⇒ logic.propositional.falsezeroorT == ¬(¬¬q ∧ ¬q) ∨ p
⇒ logic.propositional.complandT == ¬F ∨ p
⇒ logic.propositional.notfalseT == T ∨ p
⇒ logic.propositional.truezeroorT == T
24.
p ↔ q == ¬p ↔ ¬q
⇒ logic.propositional.defequiv(p ∧ q) ∨ (¬p ∧ ¬q) == ¬p ↔ ¬q
⇒ logic.propositional.defequiv(p ∧ q) ∨ (¬p ∧ ¬q) == (¬p ∧ ¬q) ∨ (¬¬p ∧ ¬¬q)
⇒ top-is-or.com(p ∧ q) ∨ (¬p ∧ ¬q) == (¬¬p ∧ ¬¬q) ∨ (¬p ∧ ¬q)
⇒ logic.propositional.notnot(p ∧ q) ∨ (¬p ∧ ¬q) == (p ∧ ¬¬q) ∨ (¬p ∧ ¬q)
⇒ logic.propositional.notnot(p ∧ q) ∨ (¬p ∧ ¬q) == (p ∧ q) ∨ (¬p ∧ ¬q)
25.
(p → q) ↔ (p → r) == (p → (q ∧ r)) ∨ ¬(p → (q ∨ r))
⇒ logic.propositional.defimpl(¬p ∨ q) ↔ (p → r) == (p → (q ∧ r)) ∨ ¬(p → (q ∨ r))
⇒ logic.propositional.defimpl(¬p ∨ q) ↔ (¬p ∨ r) == (p → (q ∧ r)) ∨ ¬(p → (q ∨ r))
⇒ logic.propositional.defimpl(¬p ∨ q) ↔ (¬p ∨ r) == ¬p ∨ (q ∧ r) ∨ ¬(p → (q ∨ r))
⇒ logic.propositional.defimpl(¬p ∨ q) ↔ (¬p ∨ r) == ¬p ∨ (q ∧ r) ∨ ¬(¬p ∨ q ∨ r)
⇒ logic.propositional.gendemorganor(¬p ∨ q) ↔ (¬p ∨ r) == ¬p ∨ (q ∧ r) ∨ (¬¬p ∧ ¬q ∧ ¬r)
⇒ logic.propositional.notnot(¬p ∨ q) ↔ (¬p ∨ r) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬q ∧ ¬r)
⇒ logic.propositional.defequiv((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (¬(¬p ∨ q) ∧ ¬(¬p ∨ r)) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬q ∧ ¬r)
⇒ logic.propositional.demorganor((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (¬¬p ∧ ¬q ∧ ¬(¬p ∨ r)) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬q ∧ ¬r)
⇒ top-is-and.com((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (¬¬p ∧ ¬(¬p ∨ r) ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬q ∧ ¬r)
⇒ top-is-and.com((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (¬¬p ∧ ¬(¬p ∨ r) ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.notnot((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (p ∧ ¬(¬p ∨ r) ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.demorganor((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (p ∧ ¬¬p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.notnot((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (p ∧ p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.idempand((¬p ∨ q) ∧ (¬p ∨ r)) ∨ (p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.andoveror((¬p ∨ q) ∧ ¬p) ∨ ((¬p ∨ q) ∧ r) ∨ (p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.absorpand¬p ∨ ((¬p ∨ q) ∧ r) ∨ (p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.andoveror¬p ∨ (¬p ∧ r) ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
⇒ logic.propositional.absorpor¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q) == ¬p ∨ (q ∧ r) ∨ (p ∧ ¬r ∧ ¬q)
26.
p ↔ (p ∧ q) == p → q
⇒ logic.propositional.defimplp ↔ (p ∧ q) == ¬p ∨ q
⇒ logic.propositional.defequiv(p ∧ p ∧ q) ∨ (¬p ∧ ¬(p ∧ q)) == ¬p ∨ q
⇒ logic.propositional.idempand(p ∧ q) ∨ (¬p ∧ ¬(p ∧ q)) == ¬p ∨ q
⇒ logic.propositional.oroverand((p ∧ q) ∨ ¬p) ∧ ((p ∧ q) ∨ ¬(p ∧ q)) == ¬p ∨ q
⇒ logic.propositional.complor((p ∧ q) ∨ ¬p) ∧ T == ¬p ∨ q
⇒ logic.propositional.truezeroand(p ∧ q) ∨ ¬p == ¬p ∨ q
⇒ logic.propositional.oroverand(p ∨ ¬p) ∧ (q ∨ ¬p) == ¬p ∨ q
⇒ logic.propositional.complorT ∧ (q ∨ ¬p) == ¬p ∨ q
⇒ logic.propositional.truezeroandq ∨ ¬p == ¬p ∨ q
⇒ top-is-or.comq ∨ ¬p == q ∨ ¬p
27.
p ↔ (p → q) == p ∧ q
⇒ logic.propositional.defimplp ↔ (¬p ∨ q) == p ∧ q
⇒ logic.propositional.defequiv(p ∧ (¬p ∨ q)) ∨ (¬p ∧ ¬(¬p ∨ q)) == p ∧ q
⇒ logic.propositional.andoveror(p ∧ ¬p) ∨ (p ∧ q) ∨ (¬p ∧ ¬(¬p ∨ q)) == p ∧ q
⇒ logic.propositional.complandF ∨ (p ∧ q) ∨ (¬p ∧ ¬(¬p ∨ q)) == p ∧ q
⇒ logic.propositional.falsezeroor(p ∧ q) ∨ (¬p ∧ ¬(¬p ∨ q)) == p ∧ q
⇒ logic.propositional.demorganor(p ∧ q) ∨ (¬p ∧ ¬¬p ∧ ¬q) == p ∧ q
⇒ logic.propositional.compland(p ∧ q) ∨ (F ∧ ¬q) == p ∧ q
⇒ logic.propositional.falsezeroand(p ∧ q) ∨ F == p ∧ q
⇒ logic.propositional.falsezeroorp ∧ q == p ∧ q
28.
(p → q) ∧ (r → q) == (p ∨ r) → q
⇒ logic.propositional.defimpl(¬p ∨ q) ∧ (r → q) == (p ∨ r) → q
⇒ logic.propositional.defimpl(¬p ∨ q) ∧ (¬r ∨ q) == (p ∨ r) → q
⇒ logic.propositional.defimpl(¬p ∨ q) ∧ (¬r ∨ q) == ¬(p ∨ r) ∨ q
⇒ logic.propositional.demorganor(¬p ∨ q) ∧ (¬r ∨ q) == (¬p ∧ ¬r) ∨ q
⇒ logic.propositional.andoveror((¬p ∨ q) ∧ ¬r) ∨ ((¬p ∨ q) ∧ q) == (¬p ∧ ¬r) ∨ q
⇒ logic.propositional.absorpand((¬p ∨ q) ∧ ¬r) ∨ q == (¬p ∧ ¬r) ∨ q
⇒ logic.propositional.andoveror(¬p ∧ ¬r) ∨ (q ∧ ¬r) ∨ q == (¬p ∧ ¬r) ∨ q
⇒ logic.propositional.absorpor(¬p ∧ ¬r) ∨ q == (¬p ∧ ¬r) ∨ q
29.
p ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ introtrueleft(T ∧ p) ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ introcompl((q ∨ ¬q) ∧ p) ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ logic.propositional.andoveror(q ∧ p) ∨ (¬q ∧ p) ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ introtrueleft(T ∧ q ∧ p) ∨ (¬q ∧ p) ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ introcompl((r ∨ ¬r) ∧ q ∧ p) ∨ (¬q ∧ p) ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ logic.propositional.andoveror(r ∧ q ∧ p) ∨ (¬r ∧ q ∧ p) ∨ (¬q ∧ p) ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ top-is-or.com(r ∧ q ∧ p) ∨ (q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬q ∧ p) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)
⇒ top-is-or.com(r ∧ q ∧ p) ∨ (q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬q ∧ p) == (q ∧ r) ∨ (p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ absorpor-subset(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬q ∧ p) == (q ∧ r) ∨ (p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ introtrueleft(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (T ∧ ¬q ∧ p) == (q ∧ r) ∨ (p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ introcompl(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ ((r ∨ ¬r) ∧ ¬q ∧ p) == (q ∧ r) ∨ (p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ logic.propositional.andoveror(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (r ∧ ¬q ∧ p) ∨ (¬r ∧ ¬q ∧ p) == (q ∧ r) ∨ (p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ introtrueleft(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (r ∧ ¬q ∧ p) ∨ (¬r ∧ ¬q ∧ p) == (q ∧ r) ∨ (T ∧ p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ introcompl(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (r ∧ ¬q ∧ p) ∨ (¬r ∧ ¬q ∧ p) == (q ∧ r) ∨ ((r ∨ ¬r) ∧ p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ logic.propositional.andoveror(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (r ∧ ¬q ∧ p) ∨ (¬r ∧ ¬q ∧ p) == (q ∧ r) ∨ (r ∧ p ∧ ¬q) ∨ (¬r ∧ p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ top-is-or.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (r ∧ p ∧ ¬q) ∨ (¬r ∧ p ∧ ¬q) ∨ (p ∧ ¬r)
⇒ top-is-or.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (¬r ∧ p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (r ∧ p ∧ ¬q)
⇒ top-is-and.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (¬r ∧ p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ absorpor-subset(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ introtrueleft(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (T ∧ p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ introcompl(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ ((q ∨ ¬q) ∧ p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ logic.propositional.andoveror(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (q ∧ p ∧ ¬r) ∨ (¬q ∧ p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ top-is-and.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (q ∧ ¬r ∧ p) ∨ (¬q ∧ p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ top-is-and.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬q ∧ p ∧ ¬r) ∨ (r ∧ ¬q ∧ p)
⇒ top-is-and.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬q ∧ ¬r ∧ p) ∨ (r ∧ ¬q ∧ p)
⇒ top-is-and.com(q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p) == (q ∧ r) ∨ (¬r ∧ q ∧ p) ∨ (¬r ∧ ¬q ∧ p) ∨ (r ∧ ¬q ∧ p)
30.
(p ∧ q) ∨ (¬q ∧ r) == (p ∧ r) ∨ (p ∧ q ∧ ¬r) ∨ (¬p ∧ ¬q ∧ r)
⇒ introtrueleft(T ∧ p ∧ q) ∨ (¬q ∧ r) == (p ∧ r) ∨ (p ∧ q ∧ ¬r) ∨ (¬p ∧ ¬q ∧ r)
⇒ introcompl((r ∨ ¬r) ∧ p ∧ q) ∨ (¬q ∧ r) == (p ∧ r) ∨ (p ∧ q ∧ ¬r) ∨ (¬p ∧ ¬q ∧ r)
⇒ logic.propositional.andoveror(r ∧ p ∧ q) ∨ (¬r ∧ p ∧ q) ∨ (¬q ∧ r) == (p ∧ r) ∨ (p ∧ q ∧ ¬r) ∨ (¬p ∧ ¬q ∧ r)
⇒ top-is-or.com(r ∧ p ∧ q) ∨ (¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (p ∧ q ∧ ¬r) ∨ (¬p ∧ ¬q ∧ r)
⇒ top-is-or.com(r ∧ p ∧ q) ∨ (¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (p ∧ q ∧ ¬r)
⇒ top-is-and.com(r ∧ p ∧ q) ∨ (¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (p ∧ ¬r ∧ q)
⇒ top-is-and.com(r ∧ p ∧ q) ∨ (¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ introtrueleft(r ∧ p ∧ q) ∨ (T ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ introcompl(r ∧ p ∧ q) ∨ ((p ∨ ¬p) ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ logic.propositional.andoveror(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ introtrueleft(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (T ∧ p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ introcompl(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == ((q ∨ ¬q) ∧ p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ logic.propositional.andoveror(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (q ∧ p ∧ r) ∨ (¬q ∧ p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ top-is-and.com(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (p ∧ r ∧ q) ∨ (¬q ∧ p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ top-is-and.com(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (r ∧ p ∧ q) ∨ (¬q ∧ p ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
⇒ top-is-and.com(r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q) == (r ∧ p ∧ q) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ ¬q ∧ r) ∨ (¬r ∧ p ∧ q)
31.
p ∧ (q ∨ s) == (q ∧ ¬s ∧ p) ∨ (p ∧ s)
⇒ command.common-literal-specialp ∧ (q ∨ s) == (p ∧ q ∧ ¬s) ∨ (p ∧ s)
⇒ andoveror.inv.common-literalp ∧ (q ∨ s) == p ∧ ((q ∧ ¬s) ∨ s)
⇒ logic.propositional.oroverandp ∧ (q ∨ s) == p ∧ (q ∨ s) ∧ (¬s ∨ s)
⇒ logic.propositional.complorp ∧ (q ∨ s) == p ∧ (q ∨ s) ∧ T
⇒ logic.propositional.truezeroandp ∧ (q ∨ s) == p ∧ (q ∨ s)