Proof step 8 from proof int2bytes-leading-zeros (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 9:

  255 < i ⊦ int2bytes(i) = int2bytes(i / 256) + int2bytes(i % 256).last '

• Proof step 10:

  ¬ 255 < i, int2bytes(i) = i2b(0) ' + i2b(0) ' + bytes, 0 ≤ i, ∀ bytes, i0. i→n(i0) < i→n(i) → int2bytes(i0) = i2b(0) ' + i2b(0) ' + bytes ∧ 0 ≤ i0 → false ⊦

• Proof step 27:

  255 < i, int2bytes(i / 256) + int2bytes(i % 256).last ' = i2b(0) ' + i2b(0) ' + bytes, 0 ≤ i, ∀ bytes, i0. i→n(i0) < i→n(i) → int2bytes(i0) = i2b(0) ' + i2b(0) ' + bytes ∧ 0 ≤ i0 → false ⊦

Rule argument

Additional information

Used terms: i