Proof step 1 from proof int2bytes-last-01 (conclusion)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ 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 3:

  ⊦ (~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 ') ) ) ) ) .last = i2b(i)

Rule argument

Additional information

Used terms: i