Proof step 33 from proof cast-help-comm (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  # int2bits(j) < i→n(i), 1 < i0, 0 < i0, 0 < i, i < i0, i ≤ i0 ⊦ mklist(¬ 0 ≤ j, i→n(i) - # int2bits(j)) + int2bits(j) = [], i = 0, i0 = 0, bits2int(lastn(i→n(i), fillsgn(i→n(i0), int2bits(j)))) = bits2int (lastn (i→n(i0), mklist((mklist(¬ 0 ≤ j, i→n(i) - # int2bits(j)) + int2bits(j)).first, i→n(i0) - i→n(i)) + mklist(¬ 0 ≤ j, i→n(i) - # int2bits(j)) + int2bits(j)))

Rule argument

Additional information

Used simplifier rules: ⊦ 1 < i → abs(i) = i;% ⊦ 0 < j → abs(j) = j;% ⊦ i→n(i) ≤ i→n(j) ↔ abs(i) ≤ abs(j);% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ n < m → (m - n) + n = m;% ⊦ # mklist(boolvar, n) = n;% ⊦ #(bits + bits0) = # bits + # bits0;