Solution (source code)

= Solution

Write the inputs as $a=2a_1+a_0$ and $b=2b_1+b_0$. Each row compares the represented value of $a$ with all four values of $b$. In <Gray code> order $00,01,11,10$ along both axes, the <Karnaugh map> is
$$
\begin{array}{c|cccc}
a_1a_0\backslash b_1b_0&00&01&11&10\\\hline
00&1&0&0&0\\
01&1&1&0&0\\
11&1&1&1&1\\
10&1&1&0&1
\end{array}
$$
The equality cases lie on the diagonal and are all one. A complete row of ones at $a=3$ and a complete column at $b=0$ provide useful checks. The outlined groups are used in the next part.

\Image[/past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/digital-systems-linear-algebra-introduction-to-formal-proof-comparator-karnaugh.png]
{title=Two-bit comparator Karnaugh map with all five essential four-cell groups}