Proof step 4 from proof rightshift-8-01-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ # bytes < n ∧ bytes2int(bytes) < 0 → fillsgn(n, bytes) = mklist(i2b(~1), n - # bytes) + bytes

• Proof step 6:

  ¬(# int2bytes(i) < i→n(j) + # int2bytes(i) ∧ bytes2int(int2bytes(i)) < 0), # int2bytes(i) ≤ i→n(j) ⊦ i >> 8 * j = bytes2int(firstn(# int2bytes(i), fillsgn(i→n(j) + # int2bytes(i), int2bytes(i))))

• Proof step 26:

  # int2bytes(i) < i→n(j) + # int2bytes(i) ∧ bytes2int(int2bytes(i)) < 0, # int2bytes(i) ≤ i→n(j) ⊦ i >> 8 * j = bytes2int(firstn(# int2bytes(i), mklist(i2b(~1), i→n(j) + # int2bytes(i) - # int2bytes(i)) + int2bytes(i)))

Rule argument

Additional information

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