Proof step 4 from proof cast-law-shift-snd-r (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

  n→i((# int2bits(j0))-1) ≤ i, 0 ≤ j0 ⊦ band(cast(i, j), j0) = band(j, j0)

• Proof step 6:

  ¬(n→i((# int2bits(31))-1) ≤ i ∧ 0 ≤ 31), 5 ≤ i, 0 < i, 0 ≤ i ⊦ j0 i>> j = bits2int(sublist(0, # int2bits(j0), mklist(int2bits(j0).first, i→n(band(cast(i, j), 31))) + int2bits(j0)))

• Proof step 8:

  n→i((# int2bits(31))-1) ≤ i ∧ 0 ≤ 31, 5 ≤ i, 0 < i, 0 ≤ i ⊦ j0 i>> j = bits2int(sublist(0, # int2bits(j0), mklist(int2bits(j0).first, i→n(band(j, 31))) + int2bits(j0)))

Rule argument

Additional information

Used terms: 31, j, i