Extend the vocabulary from Section $8\mathrm{.}4$ to define addition for n$-$bit binary numbers.

Then encode the description of the four$-$bit adder in Figure $8\mathrm{.}6,$ and pose the queries needed to verify that it is in fact correct