Proof step 13 from proof cast-mult-pos (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 14:

  0 ≤ j, 2 ^ (i - 1) - 1 < j % 2 ^ i, 0 < i ⊦ cast(i, j) = j % 2 ^ i - 2 ^ i

• Proof step 15:

  ¬(0 ≤ j * 2 ^ i + j0 ∧ 2 ^ (i - 1) - 1 < (j * 2 ^ i + j0) % 2 ^ i ∧ 0 < i), 0 ≤ j, 0 ≤ j0, 0 < i, 2 ^ (i - 1) ≤ j0 % 2 ^ i ⊦ j0 % 2 ^ i = cast(i, j * 2 ^ i + j0) + 2 ^ i

• Proof step 16:

  0 ≤ j * 2 ^ i + j0 ∧ 2 ^ (i - 1) - 1 < (j * 2 ^ i + j0) % 2 ^ i ∧ 0 < i, 0 ≤ j, 0 ≤ j0, 0 < i, 2 ^ (i - 1) ≤ j0 % 2 ^ i ⊦ j0 % 2 ^ i = ((j * 2 ^ i + j0) % 2 ^ i - 2 ^ i) + 2 ^ i

Rule argument

Additional information

Used terms: j * 2 ^ i + j0, i