Proof step 43 from proof int2bytes-len-ls-01 (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 44:

  n→i(n) ≤ i0, # int2bits(i) / 8 = i→n(i0), # int2bits(i) ≤ i→n(8 * i0) + 1, 0 < i, i→n(8 * i0 - 1) + 1 < # int2bits(i), 0 < i0 ⊦ ¬ i < 2 ^ (n→i(n) * 8 - 1), i0 = 0, i = 0, # int2bits(i) % 8 = 0

• Proof step 73:

  ¬ i < 2 ^ (n→i(n) * 8 - 1), # int2bits(i) / 8 = i→n(i0), # int2bits(i) ≤ i→n(8 * i0) + 1, 0 < i, i→n(8 * i0 - 1) + 1 < # int2bits(i), 0 < i0 ⊦ n→i(n) ≤ i0, i0 = 0, i = 0, # int2bits(i) % 8 = 0

Rule argument

Additional information