Exercise 8.33 [4bit-adder-exercise]

Extend the vocabulary from Section circuits-section to define addition for $n$-bit binary numbers. Then encode the description of the four-bit adder in Figure 4bit-adder-figure, and pose the queries needed to verify that it is in fact correct.

Figure [adder-figure] A four-bit adder. Each ${Ad}_i$ is a one-bit adder, as in figure [adder-figure](#adder-figure) on page [adder-figure](#/)