Proof step 2 from proof fix-bits2bytes (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 - 1) ⊦ bits = [], n = 0, fix(n, bits2bytes(bits)) = bits2bytes(fillsgn(n * 8, bits))

• Proof step 86:

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

Rule argument

Additional information

Used terms: bits2bytes(bits), n