Proof step 191 from proof int2bytes-rec-neg-05 (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 192:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≠ j → (i ≤ j ↔ i < j);% ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0;%n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0;% ⊦ m + 1 ≠ 0;% ⊦ m * n = n * m;% ⊦ m0 * m * n = (m0 * m) * n;%n ≠ 0 ⊦ (m + n0 * n) % n = m % n;% ⊦ m < n → n ≠ 0; (forward)% ⊦ m < n ∧ n = n0 → m < n0; (forward)% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i * j = j * i;% ⊦ (bytes + bytes0) + bytes1 = bytes + bytes0 + bytes1;% ⊦ #(bytes + bytes0) = # bytes + # bytes0;