Proof step 81 from proof bytes2int-int2bytes-len-eq (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 82:

  ⊦ i % j = 0 ∧ i + i0 < 0 ∧ i0 % j ≠ 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j + 1

• Proof step 83:

  (bytes2int(bytes1) * 256) % 256 = 0 ∧ bytes2int(bytes1) * 256 + band(b2i(by), 255) < 0 ∧ band(b2i(by), 255) % 256 ≠ 0 ∧ bytes2int(bytes1) * 256 < 0 ∧ 0 ≤ band(b2i(by), 255) ∧ 0 < 256, # bytes1 = # int2bytes((bytes2int(bytes1) * 256) / 256 + band(b2i(by), 255) / 256 + 1), (bytes2int(bytes1) * 256 + band(b2i(by), 255)) % 256 = 0, bytes2int(bytes1) * 256 + band(b2i(by), 255) < ~256, bytes2int(bytes1) * 256 + band(b2i(by), 255) < 0, bytes2int(bytes1) < 0, ∀ bytes0. # bytes0 < #(bytes1 + by ') → true → # bytes0 = # int2bytes(bytes2int(bytes0)) → bytes0 = int2bytes(bytes2int(bytes0)) ⊦ bytes2int(bytes1) * 256 + band(b2i(by), 255) = ~256, bytes1 = [], bytes1 + by ' = int2bytes((bytes2int(bytes1) * 256) / 256 + band(b2i(by), 255) / 256 + 1) + i2b(0) ', band(b2i(by), 255) % 256 = 0

Rule argument

Additional information

Used simplifier rules: ⊦ i * j = j * i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ band(i, j) = band(j, i);%i0 % j = 0, j ≠ 0 ⊦ (i * (* i0)) % (* j) = 0;% ⊦ i * j * j0 = (i * j) * j0;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ i < j → (¬ ¬ j ≤ i ↔ false);% ⊦ 0 < i → (i * j < 0 ↔ j < 0);% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ 0 ≤ i → ¬ band(i, j) < 0;% ⊦ band(i, band(i0, j)) = band(band(i, i0), j); Used terms: 256, band(b2i(by), 255), bytes2int(bytes1) * 256