Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2023/digital-systems-linear-algebra-and-introduction-to-formal-proof/1/b/solution

A logical right shift by moves into position and fills the high positions with zero. Its unsigned interpretation is
Meanwhile the original unsigned interpretation decomposes as
By integer division, , exactly the unsigned quotient. Thus the source instruction puts the required quotient into r1. This is a proof from binary representation, rather than an assumption that every kind of right shift implements every kind of division. The displayed bit argument applies to , with endpoint operations implemented as a copy or zero where appropriate.

New to topics? Read the docs here!