Proof step 8 from proof uint2bits-add-low-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

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

• Proof step 16:

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

Rule argument

Additional information

Used terms: 2 ^ i + j0, i, j - 1