Proof step 2 from proof int2bytes-rec-neg-03 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  j < ~(2 ^ (i * 8)), 0 < i, j % 2 ^ (i * 8) ≠ 0 ⊦ int2bytes(j) = int2bytes(j / 2 ^ (i * 8) - 1) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest

• Proof step 4:

  ¬(j < ~(2 ^ (i * 8)) ∧ 0 < i ∧ j % 2 ^ (i * 8) ≠ 0), 0 < i, j + 2 ^ (i * 8) < 0 ⊦ int2bytes(j) = int2bytes((j + 1 - 2 ^ (i * 8)) / 2 ^ (i * 8)) + fix(i→n(i) + 1, int2bytes(j % 2 ^ (i * 8))).rest

• Proof step 27:

  j < ~(2 ^ (i * 8)) ∧ 0 < i ∧ j % 2 ^ (i * 8) ≠ 0, 0 < i, j + 2 ^ (i * 8) < 0 ⊦ int2bytes(j / 2 ^ (i * 8) - 1) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest = int2bytes((j + 1 - 2 ^ (i * 8)) / 2 ^ (i * 8)) + fix(i→n(i) + 1, int2bytes(j % 2 ^ (i * 8))).rest

Rule argument

Additional information

Used terms: j, i