Proof step 2 from proof uint2bits-add-high-02 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ j0 < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j0) ∧ abs(j0) ≤ 2 ^ i ∧ 1 < j → uint2bits(j * 2 ^ i + j0) = uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest)

• Proof step 4:

  ¬(j0 < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j0) ∧ abs(j0) ≤ 2 ^ i ∧ 1 < j), 0 < j, j0 < 0, 0 < i, 2 ^ (i - 1) + j0 < 0, 0 ≤ j0 + 2 ^ i ⊦ uint2bits(j * 2 ^ i + j0) = sgn(uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest))

• Proof step 28:

  j0 < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j0) ∧ abs(j0) ≤ 2 ^ i ∧ 1 < j, 0 < j, j0 < 0, 0 < i, 2 ^ (i - 1) + j0 < 0, 0 ≤ j0 + 2 ^ i ⊦ uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest) = sgn(uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest))

Rule argument

Additional information

Used terms: j0, i, j