Proof step 11 from proof int2int-neg (previous step)

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

User applied rule insert rewrite lemma

Proof step 12:
⊦ 0 < i → bits2int(uint2bits(i).rest) = i - 2 ^ (n→i(# uint2bits(i)) - 1)
Proof step 13:
¬ 0 < 2 ^ n→i(# int2bits(~ j)) + j, 0 ≤ 2 ^ n→i(# int2bits(~ j)) + j ⊦ j < 0 → bits2int(int2bits(j)) = bits2int(uint2bits(2 ^ n→i(# int2bits(~ j)) + j).rest)
Proof step 21:
0 < 2 ^ n→i(# int2bits(~ j)) + j, 0 ≤ 2 ^ n→i(# int2bits(~ j)) + j ⊦ j < 0 → bits2int(int2bits(j)) = 2 ^ n→i(# int2bits(~ j)) + j - 2 ^ (n→i(# uint2bits(2 ^ n→i(# int2bits(~ j)) + j)) - 1)

name: uint2int-rest rotate: F subst: [i] → [2 ^ n→i(# int2bits(~ j)) + j]

Used terms: 2 ^ n→i(# int2bits(~ j)) + j