Proof step 259 from proof bitsand-cast (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 260:

  n0 + # bits = # fillsgn(n0 + # bits, mklist(false, m) + false ' + true ' + bits1), 2 + # bits1 = # bits, 2 + # bits1 + m < n0 + # bits, m + # bitsand(bits, false ' + true ' + bits1) ≤ n0 + # bits, m ≤ # bits2 ∨ bits2.first ⊦ bits2 + bits = [], m = 0, bits = [], mklist(false, m) + bitsand(bits, false ' + true ' + bits1) = [], bits2 = [], mklist(false, n0) = mklist(false, n0 + # bits - m + # bitsand(bits, false ' + true ' + bits1)) + mklist(false, m)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1;% ⊦ bits + bits0 = bits1 + bits0 ↔ bits = bits1;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ m ≤ n → (n < m ↔ false);% ⊦ # mklist(boolvar, n) = n;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ n ≠ 0 → ((mklist(boolvar, n) + bits).first ↔ boolvar);% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;