Proof step 2 from proof int2bytes-butlast (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ int2bytes(i) = (~128 ≤ i ∧ i < 128 ⊃ i2b(i) ' ;(128 ≤ i ∧ i < 256 ⊃ i2b(0) ' + i2b(i - 256) ' ;(~256 < i ∧ i < ~128 ⊃ i2b(~1) ' + i2b(i) ' ;(i < ~256 ∧ i % 256 = 0 ⊃ int2bytes(i / 256) + int2bytes(i % 256).last ' ;(i < ~256 ∧ i % 256 ≠ 0 ⊃ int2bytes(i / 256 - 1) + int2bytes(i % 256).last ';int2bytes(i / 256) + int2bytes(i % 256).last ') ) ) ) )

• Proof step 4:

  i < ~128 ∨ 128 ≤ i ⊦ (~128 ≤ i ∧ i < 128 ⊃ i2b(i) ' ;(128 ≤ i ∧ i < 256 ⊃ i2b(0) ' + i2b(i - 256) ' ;(~256 < i ∧ i < ~128 ⊃ i2b(~1) ' + i2b(i) ' ;(i < ~256 ∧ i % 256 = 0 ⊃ int2bytes(i / 256) + int2bytes(i % 256).last ' ;(i < ~256 ∧ i % 256 ≠ 0 ⊃ int2bytes(i / 256 - 1) + int2bytes(i % 256).last ';int2bytes(i / 256) + int2bytes(i % 256).last ') ) ) ) ) .butlast = int2bytes(i >> 8)

Rule argument

Additional information

Used terms: i