Proof step 149 from proof uint2bits-add-high (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 150:

  ⊦ 0 ≤ j ∧ 0 ≤ j0 → i ^ (j + j0) = i ^ j * i ^ j0

• Proof step 151:

  0 ≤ i2 ∧ 0 ≤ 2, 1 = i + i1 * 2, 0 ≤ 2 ^ i2 * 2 ^ 2, 0 < 2 ^ i2 * 2 ^ 2, 2 + 2 ^ (1 + i2) < 2 ^ i2 * 2 ^ 2, i1 * 2 ≤ 2 ^ i2 * 2 ^ 2 + 1, 2 + 2 ^ (1 + i2) < i1 * 2 + 2 ^ i2 * 2 ^ 2, 2 < i1 * 2 + 2 ^ i2 * 2 ^ 2, 2 + 2 ^ (1 + i2) < 2 * (i1 + 1) + i2, 2 < 2 * (i1 + 1) + i2, 2 ^ (1 + i2) < i1 * 2 + 2 ^ i2 * 2 ^ 2, 2 ^ (1 + i2) < i1 * 2, 1 < 2 ^ i2 * 2 ^ 2, 0 ≤ i1, ~2 < i2, i1 * 2 < 2 ^ i2 * 2 ^ 2, 0 < i1, 1 + 2 ^ (1 + i2) < i1 * 2, 0 < i1 * 2 + 2 ^ i2 * 2 ^ 2, 0 ≤ 2 * (i1 + 1) + i2, 0 < 2 * (i1 + 1) + i2, 2 ^ (1 + i2) ≤ 2 ^ i2 * 2 ^ 2, ∀ i0, j. i→n(i0) < i→n(i2 + 2) → true → j < 0 ∧ 0 < i0 ∧ 2 ^ (i0 - 1) < abs(j) ∧ abs(j) ≤ 2 ^ i0 → uint2bits(j + 2 ^ i0) = sgn(int2bits(j).rest) ⊦ ~1 = i2, uint2bits(2 ^ (1 + i2) - i1) + (i % 2 ≠ 0)' = sgn(int2bits(i).rest), 2 ^ i2 * 2 ^ 2 = i1 * 2, ¬ i1 ≤ 2 ^ i2 ∧ ¬ 2 ^ (1 + i2) < i1

Rule argument

Additional information

Used simplifier rules: ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ i < 0 → (~2 < i ↔ i = ~1); Used terms: 2, i2, 2