Exercise logic.propositional.proof.unicode

Description
Prove two propositions equivalent (unicode support)

Examples

easy (7)

¬(p ∧ q) ∨ s ∨ ¬r == (p ∧ q) → (r → s)

¬(p ∨ ¬(p ∨ ¬q)) == ¬(p ∨ q)

p ∧ q == ¬(p → ¬q)

q ∧ p == p ∧ (q ∨ q)

¬(¬p ∧ ¬(q ∨ r)) == p ∨ q ∨ r

¬(p ∧ (q ∨ r)) == ¬p ∨ (¬q ∧ ¬r)

p ↔ q == ¬p ↔ ¬q

medium (14)

¬((p → q) → (p ∧ q)) == (p → q) ∧ (¬p ∨ ¬q)

¬((p ↔ q) → (p ∨ (p ↔ q))) == F

(p ∧ q) → p == T

(p → q) → (p → s) == (¬q → ¬p) → (¬s → ¬p)

¬(p ∨ (¬p ∧ q)) == ¬(p ∨ q)

(p → q) ∨ ¬p == (p → q) ∨ q

(p → q) ∨ (q → p) == T

(p → ¬q) → q == (s ∨ (s → (q ∨ p))) ∧ q

(p → q) → ¬p == p → (q → ¬p)

(¬q ∧ p) → p == (¬q ↔ q) → p

p ↔ (p ∧ q) == p → q

p ↔ (p → q) == p ∧ q

(p → q) ∧ (r → q) == (p ∨ r) → q

p ∧ (q ∨ s) == (q ∧ ¬s ∧ p) ∨ (p ∧ s)

difficult (10)

(p ∧ ¬q) ∨ (q ∧ ¬p) == (p ∨ q) ∧ ¬(p ∧ q)

(p ∧ q ∧ r) ∨ (¬p ∧ q) == (¬p ∧ q ∧ ¬r) ∨ (q ∧ r)

p ↔ q == (p → q) ∧ (q → p)

(q → (¬p → q)) → p == ¬p → (q ∧ p ∧ q ∧ q)

p → (q → r) == (p → q) → (p → r)

¬((p → q) → ¬(q → p)) == p ↔ q

p ↔ (q ↔ p) == q

(p → q) ↔ (p → r) == (p → (q ∧ r)) ∨ ¬(p → (q ∨ r))

p ∨ (q ∧ r) == (p ∧ ¬q) ∨ (p ∧ ¬r) ∨ (q ∧ r)

(p ∧ q) ∨ (¬q ∧ r) == (p ∧ r) ∨ (p ∧ q ∧ ¬r) ∨ (¬p ∧ ¬q ∧ r)