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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 314:

  # int2bits(j % 2 ^ (i * 8)) = m * 8 + n, i→n(i * 8) % 8 = 0, n < 8 + m * 8, n < m * 8 + 7, n < 8, m < i→n(i), 0 ≤ j % 2 ^ (i * 8), 2 ^ (i * 8) ≤ j, 0 < i, m * 8 + n < i→n(i * 8), 0 ≤ bytes2int(bits2bytes(int2bits(j % 2 ^ (i * 8)))) ⊦ m = 0, i = 0, m * 8 + n = i→n(i * 8), i→n(i * 8) + 1 = m * 8 + n, mklist(false, 8 * (i→n(i) - m + 1)) + mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)) = [], i→n(i) - m + 1 = 0, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)) = [], n = 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;