Expand description
Tactics for Logical EQ.
Functions
false == false
.(a == ¬a) => false
.(a == b) == c => a == (b == c)
.((a == b) == c) == (a == (b == c))
.(a == b) == c => (b == c) => a
.(a == b) == c => a => (b == c)
¬(a == b) ∧ a => ¬b
.¬(a == b) ∧ a => ¬b
.a => (a == ¬¬a)
.(a == b) => (a == c) == (b == c)
.(a == ¬b) => ¬(a == b)
.(a == b) => (c == a) == (c == b)
.(a == b) => ((a ⋁ ¬a) == (b ⋁ ¬b))
.(a => b) = (¬a ∨ b)
.(a => b) = (¬a ∨ b)
.- Makes it easier to traverse.
(a == b) ∧ (a == c) => (c == b)
- Makes it easier to traverse.
- See transitivity.
¬(a == b) = ¬(c == b) => (a == c)
.(false == a) => ¬a
.(true == a) => a
.(a == b) => (¬b == ¬a)
(a == b) ⋀ ¬(a == c) => ¬(b == c)
.(a == b) ⋀ ¬(b == c) => ¬(a == c)
.¬(a == b) => ¬(b == a)
.¬(a == b) => (a == ¬b)
.¬(a == b) => ¬(a ⋀ b)
.a == a
.(¬a == ¬b) => (b == a)
.(¬a == ¬b) ∧ ((a ∨ ¬a) == (b ∨ ¬b)) => (b == a)
.(¬a == ¬b) ∧ (a ∨ ¬a) ∧ (b ∨ ¬b) => (b == a)
.(¬a == ¬b) ∧ (a => (b ∨ ¬b)) ∧ (b => (b ∨ ¬b)) => (b == a)
.(a == b) == c => (b == a) == c
.a == (b == c) => a == (c == b)
.(a == b) => (b == a)
.(a == b) == (b == a)
.¬a => (a == false)
.(a == b) ∧ (b == c) ∧ (c == d) => (a == d)
.(a == b) ∧ (b == c) ∧ (c == d) ∧ (d == e) => (a == e)
.(a == b) ∧ (b == c) ∧ (c == d) ∧ (d == e) ∧ (e == f) => (a == f)
.(a == b) ∧ (b == c) => (a == c)
.(a == b) == (c == d) => (a == c) == (b == d)
.(a == b) = (c == b) => (a == c)
.- There is an
a : A
is the same asA
being true.