Proof step 10 from proof int2bytes-index-rightshift-02 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

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

• Proof step 17:

  0 ≤ # int2bytes(i) - i→n(i1) ∧ # int2bytes(i) - i→n(i1) < # int2bytes(i), 0 ≤ i1, i1 ≤ n→i(# int2bytes(i)), i1 ≤ 4, 0 < i1 ⊦ i2b(i >> 8 * (n→i(# int2bytes(i)) - n→i(# int2bytes(i) - i→n(i1)) + 1)) = i2b(i >> 8 * (i1 - 1))

Rule argument

Additional information

Used terms: # int2bytes(i) - i→n(i1), i