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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ 0 < i + 1 → i→n(i + 1) = i→n(i) + 1

• Proof step 19:

  0 < i * 8 + 1, i→n(i * 8) + 1 < # int2bits(j % 2 ^ (i * 8)), 0 ≤ i, # int2bits(j % 2 ^ (i * 8)) ≤ 1 + 8 * i→n(i), 0 < i, 2 ^ (i * 8) ≤ j, 0 < j, i→n(i * 8) + 1 ≤ 8 * i→n(i) ⊦ bits2bytes(int2bits(j / 2 ^ (i * 8)) + fillsgn(1 + 8 * i→n(i), int2bits(j % 2 ^ (i * 8))).rest) = int2bytes(j / 2 ^ (i * 8)) + fix(i→n(i) + 1, int2bytes(j % 2 ^ (i * 8))).rest, # fillsgn(i→n(i * 8) + 1, int2bits(j % 2 ^ (i * 8))).rest % 8 = 0 ∧ fillsgn(i→n(i * 8) + 1, int2bits(j % 2 ^ (i * 8))).rest ≠ []

Rule argument

Additional information

Used simplifier rules: ⊦ i * j = j * i;% ⊦ m * n = n * m;% ⊦ m + n = n + m;% ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0;% ⊦ ~1 < i ↔ 0 ≤ i;% ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j);% ⊦ i * j * j0 = (i * j) * j0;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i; Used terms: i * 8