; Exercise $2\mathrm{.}19$

;Show that the range of foo is a subset of the set of even natural numbers.

;You can do that by writing a property making this claim and checking it with ACL$2$s$.$

"Property $2\mathrm{.}19"$

; Exercise $2\mathrm{.}20$

;Show that the set of even natural numbers is a subset of the range of foo. You can

;do that by defining a function foo$-$witness that given as input an even natural number,

;say n$,$ returns a list containing a natural number, a natural number and a true list, say x$,$ y

; and z such that $($foo x y z$)$ is n$.$ This function generates a witness to the claim that n is in

;the range of foo. Next write a property formalizing the claim that foo$-$witness does what we want

;and check the property using ACL$2$s$.$

$($definec foo$-$witness XXX$)$

"Property $2\mathrm{.}20"$

XXX