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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 142:

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

• Proof step 143:

  ¬(# mklist(false, n * 8 - n0 * 8) % 8 = 0 ∧ 8 < # mklist(false, n * 8 - n0 * 8)), # bits = n0 * 8, n0 < n ⊦ bits = [], mklist(i2b(0), n - n0) = bits2bytes(mklist(false, n * 8 - n0 * 8)), n = n0, bits.first

• Proof step 149:

  # mklist(false, n * 8 - n0 * 8) % 8 = 0 ∧ 8 < # mklist(false, n * 8 - n0 * 8), # bits = n0 * 8, n0 < n ⊦ bits = [], mklist(i2b(0), n - n0) = bits2bytes(firstn(8, mklist(false, n * 8 - n0 * 8))) + bits2bytes(restn(8, mklist(false, n * 8 - n0 * 8))), n = n0, bits.first

Rule argument

Additional information

Used terms: mklist(false, n * 8 - n0 * 8)