Proof step 2 from proof bits2bytes-mklist-03 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  ¬(# mklist(true, n) % 8 ≠ 0 ∧ 8 < # mklist(true, n)) ⊦ n % 8 = 0, bits2bytes(mklist(true, n)) = i2b(~1) ' + mklist(i2b(~1), n / 8)

• Proof step 13:

  # mklist(true, n) % 8 ≠ 0 ∧ 8 < # mklist(true, n) ⊦ n % 8 = 0, bits2bytes(firstn(# mklist(true, n) % 8, mklist(true, n))) + bits2bytes(restn(# mklist(true, n) % 8, mklist(true, n))) = i2b(~1) ' + mklist(i2b(~1), n / 8)

Rule argument

Additional information

Used terms: mklist(true, n)