127 < i ⊦ i2b((* i)) = i2b(bits2int(lastn(8, int2bits(i))))
127 < 2147483584, i2b(64) = i2b(bits2int(lastn(8, int2bits(2147483584)))) ⊦
Used terms: 2147483584