Exercise logic.propositional.proof.top

Description
Prove two propositions equivalent (with top-level decomposition)

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 == p, q == q, s || ~r == ~r || s

⇒ top-is-or.com

p == p, q == q, s == s, ~r == ~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 == p, q == 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.nottrue

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

p /\ ~q == (p /\ ~q) || F, q /\ ~p == (p || q) /\ ~p

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

p == p, q == q, q /\ ~p == F || (q /\ ~p)

⇒ logic.propositional.falsezeroor

p == p, q == q, q /\ ~p == 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-literal

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

⇒ andoveror.inv.common-literal

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

⇒ logic.propositional.oroverand

q == q, (p || ~p) /\ (r || ~p) == (~p /\ ~r) || r

⇒ logic.propositional.complor

q == q, T /\ (r || ~p) == (~p /\ ~r) || r

⇒ logic.propositional.truezeroand

q == q, r || ~p == (~p /\ ~r) || r

⇒ logic.propositional.oroverand

q == q, r || ~p == (~p || r) /\ (~r || r)

⇒ logic.propositional.complor

q == q, r || ~p == (~p || r) /\ T

⇒ logic.propositional.truezeroand

q == q, r || ~p == ~p || r

⇒ top-is-or.com

q == q, r == r, ~p == ~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.complor

T || ~q == T

⇒ logic.propositional.truezeroor

T == T

8.

p -> q == ~q -> ~p, p -> s == ~s -> ~p

⇒ logic.propositional.defimpl

~p || q == ~q -> ~p, p -> s == ~s -> ~p

⇒ logic.propositional.defimpl

~p || q == ~~q || ~p, p -> s == ~s -> ~p

⇒ top-is-or.com

~p == ~p, q == ~~q, p -> s == ~s -> ~p

⇒ logic.propositional.notnot

p == p, q == q, p -> s == ~s -> ~p

⇒ logic.propositional.defimpl

p == p, q == q, ~p || s == ~s -> ~p

⇒ logic.propositional.defimpl

p == p, q == q, ~p || s == ~~s || ~p

⇒ top-is-or.com

p == p, q == q, ~p == ~p, s == ~~s

⇒ logic.propositional.notnot

p == p, q == q, p == p, s == s

9.

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.demorganor

p /\ q == ~~p /\ ~~q

⇒ logic.propositional.notnot

p == p, q == ~~q

⇒ logic.propositional.notnot

p == p, q == 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 == p, q == q

12.

p <-> q == (p -> q) /\ (q -> p)

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

p /\ q == F || (q /\ p), ~p /\ ~q == (~p || q) /\ ~q

⇒ logic.propositional.falsezeroor

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

⇒ top-is-and.com

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

p == p, q == q, ~p /\ ~q == (~p /\ ~q) || F

⇒ logic.propositional.falsezeroor

p == p, q == 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.truezeroor

T == 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.falsezeroand

F || p == p

⇒ logic.propositional.falsezeroor

p == 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.absorpor

q == (s || (s -> (q || p))) /\ q

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroor

q == T /\ q

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.complor

~p || ~q == T /\ (~q || ~p), r == r

⇒ logic.propositional.truezeroand

~p || ~q == ~q || ~p, r == r

⇒ top-is-or.com

~p == ~p, ~q == ~q, r == 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 || q) /\ p == p /\ q

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

(~p /\ ~q) || F == ~p /\ ~q, (~p || q) /\ p == p /\ q

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

p == p, q == q, F || (q /\ p) == p /\ q

⇒ logic.propositional.falsezeroor

p == p, q == q, q /\ p == p /\ q

⇒ top-is-and.com

p == p, q == q, q == q, p == p

18.

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

⇒ top-is-and.com

q == q || q, p == p

⇒ logic.propositional.idempor

q == q, p == p

19.

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

⇒ logic.propositional.demorganand

~~p || ~~(q || r) == p || q || r

⇒ logic.propositional.notnot

p == p, ~~(q || r) == q || r

⇒ logic.propositional.notnot

p == p, q || r == q || r

20.

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.demorganor

p == p, ~q /\ ~r == ~q /\ ~r

21.

p <-> (q <-> p) == q

⇒ logic.propositional.defequiv

p <-> ((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.complor

T /\ q == q

⇒ logic.propositional.truezeroand

q == 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.complor

T /\ (~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 == ~q, ~p == ~p || ~p

⇒ logic.propositional.idempor

q == q, ~p == ~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.truezeroor

T == (~q <-> q) -> p

⇒ logic.propositional.defimpl

T == ~(~q <-> q) || p

⇒ logic.propositional.defequiv

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.compland

T == ~F || p

⇒ logic.propositional.notfalse

T == T || p

⇒ logic.propositional.truezeroor

T == 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 == p, q == ~~q, p == p, q == q

⇒ logic.propositional.notnot

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

⇒ top-is-and.com

(~p || q) /\ (~p || r) == ~p || (q /\ r), ~~p /\ ~(~p || r) /\ ~q == p /\ ~q /\ ~r

⇒ top-is-and.com

(~p || q) /\ (~p || r) == ~p || (q /\ r), ~~p /\ ~(~p || r) == p /\ ~r, ~q == ~q

⇒ logic.propositional.notnot

(~p || q) /\ (~p || r) == ~p || (q /\ r), p /\ ~(~p || r) == p /\ ~r, q == q

⇒ logic.propositional.demorganor

(~p || q) /\ (~p || r) == ~p || (q /\ r), p /\ ~~p /\ ~r == p /\ ~r, q == q

⇒ logic.propositional.notnot

(~p || q) /\ (~p || r) == ~p || (q /\ r), p /\ p == p, r == r, q == q

⇒ logic.propositional.idempand

(~p || q) /\ (~p || r) == ~p || (q /\ r), p == p, r == r, q == q

⇒ logic.propositional.andoveror

((~p || q) /\ ~p) || ((~p || q) /\ r) == ~p || (q /\ r), p == p, r == r, q == q

⇒ logic.propositional.absorpand

~p || ((~p || q) /\ r) == ~p || (q /\ r), p == p, r == r, q == q

⇒ logic.propositional.andoveror

~p || (~p /\ r) || (q /\ r) == ~p || (q /\ r), p == p, r == r, q == q

⇒ logic.propositional.absorpor

~p == ~p, q == q, r == r, p == p, r == r, q == q

26.

p <-> (p /\ q) == p -> q

⇒ logic.propositional.defimpl

p <-> (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.complor

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

⇒ logic.propositional.truezeroand

q || ~p == ~p || q

⇒ top-is-or.com

q == q, ~p == ~p

27.

p <-> (p -> q) == p /\ q

⇒ logic.propositional.defimpl

p <-> (~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.compland

F || (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.falsezeroor

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

⇒ absorpor-subset

q /\ r == q /\ r, (~r /\ q /\ p) || (~q /\ p) == (p /\ ~q) || (p /\ ~r)

⇒ introtrueleft

q == q, r == r, (~r /\ q /\ p) || (T /\ ~q /\ p) == (p /\ ~q) || (p /\ ~r)

⇒ introcompl

q == q, r == r, (~r /\ q /\ p) || ((r || ~r) /\ ~q /\ p) == (p /\ ~q) || (p /\ ~r)

⇒ logic.propositional.andoveror

q == q, r == r, (~r /\ q /\ p) || (r /\ ~q /\ p) || (~r /\ ~q /\ p) == (p /\ ~q) || (p /\ ~r)

⇒ introtrueleft

q == q, r == r, (~r /\ q /\ p) || (r /\ ~q /\ p) || (~r /\ ~q /\ p) == (T /\ p /\ ~q) || (p /\ ~r)

⇒ introcompl

q == q, r == r, (~r /\ q /\ p) || (r /\ ~q /\ p) || (~r /\ ~q /\ p) == ((r || ~r) /\ p /\ ~q) || (p /\ ~r)

⇒ logic.propositional.andoveror

q == q, r == r, (~r /\ q /\ p) || (r /\ ~q /\ p) || (~r /\ ~q /\ p) == (r /\ p /\ ~q) || (~r /\ p /\ ~q) || (p /\ ~r)

⇒ top-is-or.com

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) || (r /\ ~q /\ p) == (r /\ p /\ ~q) || (~r /\ p /\ ~q) || (p /\ ~r)

⇒ top-is-or.com

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) == (~r /\ p /\ ~q) || (p /\ ~r), r /\ ~q /\ p == r /\ p /\ ~q

⇒ top-is-and.com

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) == (~r /\ p /\ ~q) || (p /\ ~r), r == r, ~q == ~q, p == p

⇒ absorpor-subset

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) == p /\ ~r, r == r, q == q, p == p

⇒ introtrueleft

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) == T /\ p /\ ~r, r == r, q == q, p == p

⇒ introcompl

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) == (q || ~q) /\ p /\ ~r, r == r, q == q, p == p

⇒ logic.propositional.andoveror

q == q, r == r, (~r /\ q /\ p) || (~r /\ ~q /\ p) == (q /\ p /\ ~r) || (~q /\ p /\ ~r), r == r, q == q, p == p

⇒ top-is-and.com

q == q, r == r, ~r /\ q == q /\ ~r, p == p, ~r /\ ~q /\ p == ~q /\ p /\ ~r, r == r, q == q, p == p

⇒ top-is-and.com

q == q, r == r, ~r == ~r, q == q, p == p, ~r /\ ~q /\ p == ~q /\ p /\ ~r, r == r, q == q, p == p

⇒ top-is-and.com

q == q, r == r, r == r, q == q, p == p, ~r /\ ~q == ~q /\ ~r, p == p, r == r, q == q, p == p

⇒ top-is-and.com

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

⇒ top-is-and.com

(r /\ p /\ q) || (~q /\ r) == (p /\ r) || (~p /\ ~q /\ r), ~r /\ p == p /\ ~r, q == q

⇒ top-is-and.com

(r /\ p /\ q) || (~q /\ r) == (p /\ r) || (~p /\ ~q /\ r), ~r == ~r, p == p, q == q

⇒ introtrueleft

(r /\ p /\ q) || (T /\ ~q /\ r) == (p /\ r) || (~p /\ ~q /\ r), r == r, p == p, q == q

⇒ introcompl

(r /\ p /\ q) || ((p || ~p) /\ ~q /\ r) == (p /\ r) || (~p /\ ~q /\ r), r == r, p == p, q == q

⇒ logic.propositional.andoveror

(r /\ p /\ q) || (p /\ ~q /\ r) || (~p /\ ~q /\ r) == (p /\ r) || (~p /\ ~q /\ r), r == r, p == p, q == q

⇒ introtrueleft

(r /\ p /\ q) || (p /\ ~q /\ r) == T /\ p /\ r, p == p, q == q, r == r, r == r, p == p, q == q

⇒ introcompl

(r /\ p /\ q) || (p /\ ~q /\ r) == (q || ~q) /\ p /\ r, p == p, q == q, r == r, r == r, p == p, q == q

⇒ logic.propositional.andoveror

(r /\ p /\ q) || (p /\ ~q /\ r) == (q /\ p /\ r) || (~q /\ p /\ r), p == p, q == q, r == r, r == r, p == p, q == q

⇒ top-is-and.com

r /\ p == p /\ r, q == q, p /\ ~q /\ r == ~q /\ p /\ r, p == p, q == q, r == r, r == r, p == p, q == q

⇒ top-is-and.com

r == r, p == p, q == q, p /\ ~q /\ r == ~q /\ p /\ r, p == p, q == q, r == r, r == r, p == p, q == q

⇒ top-is-and.com

r == r, p == p, q == q, p == p, ~q == ~q, r == r, p == p, q == q, r == r, r == r, p == p, q == q

31.

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

⇒ command.common-literal-special

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

⇒ andoveror.inv.common-literal

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

⇒ logic.propositional.oroverand

p == p, q || s == (q || s) /\ (~s || s)

⇒ logic.propositional.complor

p == p, q || s == (q || s) /\ T

⇒ logic.propositional.truezeroand

p == p, q || s == q || s