Proof step 2 from proof int2bits-add-high (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ j < 0 → int2bits(j) = sgn(int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest)

• Proof step 4:

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

• Proof step 7:

  j * 2 ^ i + j0 < 0, j < 0, j0 < 0, 0 < i, 2 ^ (i - 1) + j0 < 0, 0 < 2 ^ i + j0 ⊦ sgn(int2bits(2 ^ n→i(# int2bits(~(j * 2 ^ i + j0))) + j * 2 ^ i + j0).rest) = int2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest)

Rule argument

Additional information

Used terms: j * 2 ^ i + j0