Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 1 / a / Solution

Write the bit vector as $a=(a_{n-1},\dots ,a_0)$, with $a_0$ the least significant bit. Its unsigned interpretation of a bit string is $\mathrm{bin}(a)={\sum }_{i=0}^{n-1}{a}_i{2}^i$, where each $a_i\in \{0,1\}$. The range is the integers from $0$ through $2^n-1$; a leading one contributes positive weight $2^{n-1}$, not a sign.