Proof step 1 from proof int2bits-rec-2pot-neg-03 (conclusion)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ j ≤ ~(2 ^ i) ∧ 0 < i ∧ j % 2 ^ i ≠ 0 → int2bits(j) = int2bits(j / 2 ^ i - 1) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest

• Proof step 3:

  ¬(j ≤ ~(2 ^ i) ∧ 0 < i ∧ j % 2 ^ i ≠ 0) ⊦ j ≤ ~(2 ^ i) ∧ 0 < i → int2bits(j) = int2bits((j - (2 ^ i - 1)) / 2 ^ i) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest

• Proof step 7:

  j ≤ ~(2 ^ i) ∧ 0 < i ∧ j % 2 ^ i ≠ 0 ⊦ j ≤ ~(2 ^ i) ∧ 0 < i → int2bits(j / 2 ^ i - 1) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest = int2bits((j - (2 ^ i - 1)) / 2 ^ i) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest

Rule argument

Additional information

Used terms: j, i