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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 207:

  2 + # bits1 = # bits, sgn(mklist(false, m) + false ' + true ' + bits1) = false ' + true ' + bits1, n = # fillsgn(n, mklist(false, m) + false ' + true ' + bits1), n = # fillsgn(n, bitsand(bits, false ' + true ' + bits1)), 2 + # bits1 + m < # bits + # bitsand(mklist(false, m), bits2), m + 1 < # bitsand(mklist(false, m), bits2), 2 + # bits1 + m < n, m < # bitsand(mklist(false, m), bits2), n < # bits + # bitsand(mklist(false, m), bits2), 3 + # bits1 + m < # bits + # bitsand(mklist(false, m), bits2) ⊦ n = # fillsgn(n, bitsand(mklist(false, m), bits2) + bitsand(bits, false ' + true ' + bits1)), bits = [], m = 0, bits2 = [], bits2 + bits = [], fillsgn(n, bitsand(bits, false ' + true ' + bits1)) = lastn(n, fillsgn(n, bitsand(mklist(false, m), bits2) + bitsand(bits, false ' + true ' + bits1))), bitsand(mklist(false, m), bits2) = []

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m;% ⊦ m +1 = m + 1;% ⊦ m < n → n ≠ 0;% ⊦ # bits = 0 ↔ bits = [];% ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward)% ⊦ n < n0 ∧ n0 < n1 → n +1 < n1; (forward)% ⊦ m < n ∧ m = n0 → n0 < n; (forward)% ⊦ m < n → n ≠ 0; (forward)% ⊦ (boolvar ' + bits).first ↔ boolvar;%n0 < n ⊦ m + (* n) < m0 + (* n0) ↔ m + (n - n0) < m0;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n < m + n0 ↔ n < n0;% ⊦ m + n = n + m;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ boolvar ' + bits ≠ [];% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;