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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 169:

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

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 ≤ m + n0 ↔ n ≤ n0;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ m ≤ n → (n < m ↔ false);% ⊦ m + n = m + n0 ↔ n = n0;% ⊦ m + n - n + n1 = m - n1;% ⊦ # 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;