Expand description
Tactics for Logical AND.
Functions
(a ∧ b) ∧ c => a ∧ (b ∧ c)
.a ∧ (b ∨ c) => (a ∧ b) ∨ (a ∧ c)
.(a == b) => (a ∧ c) == (b ∧ c)
.¬c => (a ∧ c) == (b ∧ c)
.(a == b) => (c ∧ a) == (c ∧ b)
.¬c => (c ∧ a) == (c ∧ b)
.(¬a ∧ ¬b) ∧ (a ∨ b) => false
¬a ∧ (a ∨ b) => b
.¬b ∧ (a ∨ b) => a
(false ∧ a) => false
.¬(a ∨ b) => (¬a ∧ ¬b)
.¬(a => b) => (a ∧ ¬b)
.(a ∧ b) => a
.- Makes it easier to traverse.
(a ∧ b) ∧ (a => c) => (c ∧ b)
.- Makes it easier to traverse.
(a ∧ b) ∧ (b => c) => (a ∧ c)
.(a ∧ ¬a) => false
.(¬¬a ∧ ¬a) => false
.a ∧ (b ∧ c) => (a ∧ b) ∧ c
.(a ∧ b) ∨ (a ∧ c) => a ∧ (b ∨ c)
.((a ∧ c) == (b ∧ c)) ∧ c => (a == b)
.((c ∧ a) == (c ∧ b)) ∧ c => (a == b)
.(a ∧ b) => b
.a ∧ b => b ∧ a
.(¬a ∧ ¬b) => ¬(a ∨ b)
.(¬a ∧ ¬b) => (a == b)
.(a ∧ b) => (a == b)
.(a ∧ ¬b) => ¬(a => b)
.(a ∧ b) => (a ∨ b)
.(true ∧ a) => a
.