Documentation

Projects.Paramodulator.Basic

source
theorem Paramodulator.zero_def :
0 = Node.nil
source
theorem Paramodulator.one_def :
1 = Node.pair 0 0
source
@[simp]
theorem Paramodulator.sizeOf_zero :
sizeOf 0 = 1
source
@[simp]
theorem Paramodulator.sizeOf_one :
sizeOf 1 = 3
source
@[simp]
theorem Paramodulator.pair_ne_zero {a b : Node} :
a.pair b ≠ 0
source
@[simp]
theorem Paramodulator.zero_ne_pair {a b : Node} :
0 ≠ a.pair b
source
@[simp]
theorem Paramodulator.pair_eq_one_iff {a b : Node} :
a.pair b = 1 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem Paramodulator.one_eq_pair_iff {a b : Node} :
1 = a.pair b ↔ a = 0 ∧ b = 0
source
@[simp]
theorem Paramodulator.const_ne_zero {n : ℕ} :
const n ≠ 0
source
@[simp]
theorem Paramodulator.zero_ne_const {n : ℕ} :
0 ≠ const n
source
@[simp]
theorem Paramodulator.const_eq_one_iff {n : ℕ} :
const n = 1 ↔ n = 0
source
@[simp]
theorem Paramodulator.one_eq_const_iff {n : ℕ} :
1 = const n ↔ n = 0
source
theorem Paramodulator.const_eq_iff {n m : ℕ} :
const n = const m ↔ n = m