Proof step 5 from proof int2bytes-byte-neg (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ # bits % 8 ≠ 0 ∧ 8 < # bits → bits2bytes(bits) = bits2bytes(firstn(# bits % 8, bits)) + bits2bytes(restn(# bits % 8, bits))

• Proof step 7:

  ¬(# int2bits(i) % 8 ≠ 0 ∧ 8 < # int2bits(i)), # int2bits(i) = 9, ~256 < i, i < ~128, i < 0 ⊦ bits2bytes(int2bits(i)) = i2b(~1) ' + i2b(i) '

• Proof step 8:

  # int2bits(i) % 8 ≠ 0 ∧ 8 < # int2bits(i), # int2bits(i) = 9, ~256 < i, i < ~128, i < 0 ⊦ bits2bytes(firstn(# int2bits(i) % 8, int2bits(i))) + bits2bytes(restn(# int2bits(i) % 8, int2bits(i))) = i2b(~1) ' + i2b(i) '

Rule argument

Additional information

Used terms: int2bits(i)