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

Split each input into its more and less significant $n$-bit halves: $a=2^n{a}_H+a_L$ and $b=2^n{b}_H+b_L$. Let the two digital comparators produce $(L_H,G_H)$ and $(L_L,G_L)$. The more significant halves are equal exactly when $E_H=\neg (L_H\vee G_H)$. The comparator composition is thereforeImplement $E_H$ with a logical disjunction followed by a negation, then use two AND gates and two more logical disjunction logic gates. If $a_H\ne b_H$, the difference $2^n(a_H-b_H)$ has magnitude at least $2^n$, whereas $|a_L-b_L|\le 2^n-1$; hence the more significant comparison decides the result. If $a_H=b_H$, the lower comparison decides it. This proves correctness in every case using a constant number of extra logic gates.