Exercise 8.34

The circuit representation in the chapter is more detailed than necessary if we care only about circuit functionality. A simpler formulation describes any $m$-input, $n$-output gate or circuit using a predicate with $m+n$ arguments, such that the predicate is true exactly when the inputs and outputs are consistent. For example, NOT gates are described by the binary predicate ${NOT}(i,o)$, for which ${NOT}(0,1)$ and ${NOT}(1,0)$ are known. Compositions of gates are defined by conjunctions of gate predicates in which shared variables indicate direct connections. For example, a NAND circuit can be composed from ${AND}$s and ${NOT}$s: ${\forall\,i_1,i_2,o_a,o\;\;} {AND}(i_1,i_2,o_a) \land {NOT}(o_a,o) {\:\;{\Rightarrow}\:\;}{NAND}(i_1,i_2,o)\ .$ Using this representation, define the one-bit adder in Figure adder-figure and the four-bit adder in Figure 4bit-adder-figure, and explain what queries you would use to verify the designs. What kinds of queries are not supported by this representation that are supported by the representation in Section circuits-section?