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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 248:

  ⊦ n % 8 = 0 ∧ n ≠ 0 → bits2bytes(mklist(true, n)) = mklist(i2b(~1), n / 8)

• Proof step 249:

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

• Proof step 255:

  (n * 8 - n0 * 8) % 8 = 0 ∧ n * 8 - n0 * 8 ≠ 0, # bits = n0 * 8, bits.first, n0 < n ⊦ bits = [], mklist(i2b(~1), n - n0) = mklist(i2b(~1), (n * 8 - n0 * 8) / 8), n = n0

Rule argument

Additional information

Used terms: n * 8 - n0 * 8