| bitsand(boolvar ' + bits3.butlast, false ' + bits0.butlast) = true ' + bits1.butlast, bits0.last ∧ bits3.last ↔ bits1.last, ∀ bits2, bits0, bits1. # bits2 < #(boolvar + bits3) → bitsand(bits2, false ' + bits0) = true ' + bits1 → bits2 = [] ⊦ bits1 = [], bits3 = [], bits0 = [], ¬ (bits3.last ∧ bits0.last) ∈ bits1 ∧ (¬ bits3.last ∨ ¬ bits0.last) |
Used simplifier rules: ⊦ bits ≠ [] → (bits.butlast = [] ↔ bits = bits.first ');% ⊦ boolvar ' ≠ [];% ⊦ ¬ bits + bits0 ≠ [] ↔ bits = [] ∧ bits0 = [];% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ # boolvar ' = 0 +1;% ⊦ bits ≠ [] → # bits.butlast = # bits - 1;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ m + n < m + n0 ↔ n < n0;% ⊦ ¬ m < n ↔ n ≤ m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = n + m;% ⊦ m ≤ m - 1 → m = 0; (forward)% ⊦ # bits = 0 ↔ bits = [];% ⊦ m < 1 ↔ m = 0;% ⊦ ¬ m ≤ n ↔ n < m;%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0;% ⊦ m < n + 1 ↔ ¬ n < m;% ⊦ ¬ n < n; Used terms: boolvar ' + bits3.butlast, bits0.butlast, bits1.butlast