Proof step 2 from proof int2bytes-index-rightshift (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ i→n(j) < # int2bytes(i) → i >> 8 * j = bytes2int(firstn(# int2bytes(i) - i→n(j), int2bytes(i)))

• Proof step 4:

  ¬ i→n(n→i(# int2bytes(i)) - j + 1) < # int2bytes(i), 0 ≤ j, j < n→i(# int2bytes(i)) ⊦ int2bytes(i)[i→n(j)] = i2b(i >> 8 * (n→i(# int2bytes(i)) - j + 1))

• Proof step 14:

  i→n(n→i(# int2bytes(i)) - j + 1) < # int2bytes(i), 0 ≤ j, j < n→i(# int2bytes(i)) ⊦ int2bytes(i)[i→n(j)] = i2b(bytes2int(firstn(# int2bytes(i) - i→n(n→i(# int2bytes(i)) - j + 1), int2bytes(i))))

Rule argument

Additional information

Used terms: n→i(# int2bytes(i)) - j + 1, i