Expand description
Tactics for Logical AND.
Re-exports
pub use commute as symmetry;
Functions
(a ∧ b) ∧ c => a ∧ (b ∧ c)
.
a ∧ b => b ∧ a
.
a ∧ (b ∨ c) => (a ∧ b) ∨ (a ∧ c)
.
(¬a ∧ ¬b) ∧ (a ∨ b) => a
¬a ∧ (a ∨ b) => b
.
¬b ∧ (a ∨ b) => a
(false ∧ a) => false
.
¬(a ∨ b) => (¬a ∧ ¬b)
.
¬(a => b) => (a ∧ ¬b)
.
(a ∧ b) ∧ (a => c) => (c ∧ b)
.
(a ∧ b) ∧ (b => c) => (a ∧ c)
.
(¬a ∧ ¬b) => ¬(a ∨ b)
.
(¬a ∧ ¬b) => (a = b)
.
(a ∧ b) => (a = b)
.
(a ∧ ¬b) => ¬(a => b)
.
(true ∧ a) => true
.