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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 192:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j;% ⊦ j < i ∧ i ≤ 0 → j < 0; (forward)% ⊦ i < j ∧ j ≤ j0 → i < j0; (forward)%i0 ≠ 0, i0 < i ⊦ (* i) < j → (* i0) < j;% ⊦ i ≤ ~1 ↔ i < 0;% ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j;% ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0;% ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0;% ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0);% ⊦ i + j < i + i0 ↔ j < i0;% ⊦ i * j = j * i;% ⊦ i * j * j0 = (i * j) * j0;% ⊦ i * j + i = i * (j + 1);% ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward)% ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward)% ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward)% ⊦ i ≤ j ∧ j < j0 → i < j0; (forward)% ⊦ band(i, j) = band(j, i);