Proof step 6 from proof int2bytes-len-one-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 7:

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

  # (~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 = b2i(i2b(i)), ¬ i < ~128 ∧ ¬ 127 < i

Rule argument

Additional information

Used terms: i