Proof step 68 from proof bor-2pot-plus-01 (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  0 < i, j0 < 2 ^ i, j < 2 ^ i, (¬ mklist(false, i→n(i)).first) ∈ bitsinvert(uint2bits(~ j)) +1, j + 1 < 2 ^ i, j < j0, j < i, 0 < 2 ^ i, 0 ≤ j0, j + 1 < i, j < 0, # int2bits(j0) ≤ i→n(i) ⊦ bitsinvert(int2bits(j)) + mklist(true, i→n(i)) = [], i = 0, (j + 1) * 2 ^ (n→i(i→n(i) - # int2bits(j0)) + n→i(# int2bits(j0))) = 1 + j * 2 ^ i + bits2uint(mklist(true, i→n(i) - # int2bits(j0)) + bitsinvert(int2bits(j0))) + j0, mklist(true, i→n(i) - # int2bits(j0)) + bitsinvert(int2bits(j0)) = []

Rule argument

Additional information

Used simplifier rules: ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ int2bits(j) ≠ [];% ⊦ bitsinvert(bits) = [] ↔ bits = [];% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ n→i(m + n) = n→i(m) + n→i(n);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # mklist(boolvar, n) = n;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ # bitsinvert(bits) = # bits;% ⊦ 0 ≤ j → bitsinvert(int2bits(j)).first;