Proof step 256 from proof int2bytes-rec-pos-any (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 257:

  # int2bits(j % 2 ^ (i * 8)) = (i→n(i) - 1) * 8 + n, n < 8 + (i→n(i) - 1) * 8, n < (i→n(i) - 1) * 8 + 7, 0 ≤ bytes2int(bits2bytes(int2bits(j % 2 ^ (i * 8)))), 2 ^ (i * 8) ≤ j, 0 ≤ j % 2 ^ (i * 8), n < 8, 0 < i ⊦ i→n(i) - 1 = 0, n = 0, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)) = [], 1 + 8 * i→n(i) = (i→n(i) - 1) * 8 + n, (i→n(i) - 1) * 8 + n = 8 * i→n(i), i = 0, bits2bytes(firstn(8, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)))) + bits2bytes(restn(8, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)))) = bits2bytes(int2bits(j % 2 ^ (i * 8)))

Rule argument

Additional information

Used simplifier rules: ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0;% ⊦ m < m + n ↔ n ≠ 0;%n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n);% ⊦ m +1 = m + 1;%n < n0 ⊦ (* n) ≠ m0 + (* n0);% ⊦ m * n = n * m;% ⊦ m0 * m * n = (m0 * m) * n;%n ≠ 0 ⊦ (m + n0 * n) % n = m % n;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ n < m → (m - n) + n = m;% ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward)% ⊦ n < n0 ∧ n0 < n1 → n +1 < n1; (forward)% ⊦ m < n → n ≠ 0; (forward)% ⊦ i * j = j * i;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # mklist(boolvar, n) = n;% ⊦ #(bits + bits0) = # bits + # bits0;