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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  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(# bitsand(bitsinvert(int2bits(j0)), mklist(true, i→n(i)))) = (j * 2 ^ i + j0) + 1 + bits2uint(bitsand(bitsinvert(int2bits(j0)), mklist(true, i→n(i)))), bitsand(bitsinvert(int2bits(j0)), mklist(true, i→n(i))) = []

Rule argument

Additional information

Used simplifier rules: ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ j < 0 → int2bits(j).first;% ⊦ int2bits(j) ≠ [];% ⊦ # bits = 0 ↔ bits = [];% ⊦ i - j = i0 ↔ i = i0 + j;% ⊦ bitsinvert(bitsinvert(bits)) = bits;% ⊦ ~ ~ i = i;% ⊦ i * j = j * i;% ⊦ i * j * j0 = (i * j) * j0;% ⊦ ~ i * j = ~(i * j);% ⊦ # bitsinvert(bits) = # bits;% ⊦ ~ i - j = ~(i + j);% ⊦ j < 0 → bits2uint(bitsinvert(int2bits(j))) = ~ j - 1;