Proof step 14 from proof int2bytes-rec255-neg (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  # int2bytes(i % 256) < 2, i < 0, i < ~128, i % 256 < 0 ⊦ ¬ i % 256 < ~256, (mklist(i2b(~1), 2 - # int2bytes(i % 256)) + int2bytes(i % 256)).rest = int2bytes(i % 256).last '

• Proof step 20:

  # int2bytes(i % 256) < 2, i < 0, i < ~128, i % 256 < 0 ⊦ ¬ ~128 ≤ i % 256, (mklist(i2b(~1), 2 - # int2bytes(i % 256)) + int2bytes(i % 256)).rest = int2bytes(i % 256).last '

Rule argument

Additional information