Proof step 2 from proof fix-bits2bytes-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  ¬(# bits2bytes(bits) < n ∧ bytes2int(bits2bytes(bits)) < 0), # bits ≤ 8 * n ⊦ n = 0, bits = [], fix(n, bits2bytes(bits)) = bits2bytes(mklist(bits.first, n * 8 - # bits) + bits)

• Proof step 172:

  # bits2bytes(bits) < n ∧ bytes2int(bits2bytes(bits)) < 0, # bits ≤ 8 * n ⊦ n = 0, bits = [], mklist(i2b(~1), n - # bits2bytes(bits)) + bits2bytes(bits) = bits2bytes(mklist(bits.first, n * 8 - # bits) + bits)

Rule argument

Additional information

Used terms: bits2bytes(bits), n