Proof step 9 from proof int2bytes-one (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 10:

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

  # (~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 ') ) ) ) ) = 1, i < ~128, i < 0 ⊦

Rule argument

Additional information

Used terms: i