Proof step 5 from proof fix-bits2bytes (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

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

• Proof step 26:

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

Rule argument

Additional information

Used terms: bits2bytes(bits), n