Proof step 6 from proof bits2bytes-mklist-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ # bits0 % 8 = 0 ∧ bits ≠ [] ∧ bits0 ≠ [] → bits2bytes(bits + bits0) = bits2bytes(bits) + bits2bytes(bits0)

• Proof step 8:

  ¬(# mklist(false, m * 8) % 8 = 0 ∧ mklist(false, n0) ≠ [] ∧ mklist(false, m * 8) ≠ []), n0 < 8 ⊦ bits2bytes(mklist(false, n0) + mklist(false, m * 8)) = i2b(0) ' + mklist(i2b(0), m), n0 = 0

• Proof step 14:

  # mklist(false, m * 8) % 8 = 0 ∧ mklist(false, n0) ≠ [] ∧ mklist(false, m * 8) ≠ [], n0 < 8 ⊦ bits2bytes(mklist(false, n0)) + bits2bytes(mklist(false, m * 8)) = i2b(0) ' + mklist(i2b(0), m), n0 = 0

Rule argument

Additional information

Used terms: mklist(false, m * 8), mklist(false, n0)