Proof step 2 from proof bits2bytes-fill (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(8, bits)) + bits2bytes(restn(8, bits))

• Proof step 4:

  ¬(#(mklist(bits.first, 8 - # bits % 8) + bits) % 8 = 0 ∧ 8 < #(mklist(bits.first, 8 - # bits % 8) + bits)) ⊦ bits2bytes(bits) = bits2bytes(mklist(bits.first, 8 - # bits % 8) + bits), # bits % 8 = 0, bits = []

• Proof step 16:

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

Rule argument

Additional information

Used terms: mklist(bits.first, 8 - # bits % 8) + bits