Figure 5: Specification of the circuit in Figure 4 in propositional logic.