; Problem 101. ; Suppose p, m, up, and dn (``down'') are undefined functions. Suppose ; however that you know this about p, m, and dn: ; ; Theorem. dn-spec ; (and (o-p (m x)) ; (implies (p x) ; (o< (m (dn x)) (m x)))) ; ; Then admit ; ; (defun f4 (x y q) ; (if (p x) ; (if q ; (f4 y (dn x) (not q)) ; (f4 y (up x) (not q))) ; 4)) ; ; Note that f4 is swapping its arguments. Thus, if q starts at t, say, ; then in successive calls the first argument is x, y, (dn x), (up y), ; (dn (dn x)), (up (up y)), etc. I thank Anand Padmanaban for helping ; me think of and solve this problem. (in-package "ACL2") (encapsulate ((p (x) t) (m (x) t) (up (x) t) (dn (x) t)) (local (defun p (x) (posp x))) ; or, (not (zp x)) (local (defun m (x) (nfix x))) ; or, (acl2-count x) (defthm o-p-m (o-p (m x))) (local (defun dn (x) (1- x))) ; or, (- x 1) (defthm dn-goes-down (implies (p x) (o< (m (dn x)) (m x)))) (local (defun up (x) (1+ x))) ; or, x ) (defthm lemma-1-1 (not (< (m x) 0)) :hints (("Goal" :use o-p-m :in-theory (disable o-p-m)))) (defthm lemma-1 (implies (p x) (not (equal 0 (m x)))) :hints (("Goal" :in-theory (disable dn-goes-down) :use dn-goes-down))) (defthm lemma-2 (implies (and (p x) (not (consp (m x)))) (< 0 (m x))) :hints (("Goal" :use (lemma-1 o-p-m) :in-theory (disable lemma-1 o-p-m)))) (defthm lemma-3-1 (not (o< x x))) (defthm lemma-3 (implies (p x) (not (equal (m (dn x)) (m x)))) :hints (("Goal" :in-theory (disable dn-goes-down) :use dn-goes-down))) (defun f4 (x y q) (declare (xargs :measure (if (p x) (if q (cons (cons (m x) 1) 0) ; (make-ord (m x) 1 0) (if (p y) (cons (cons (m y) 2) 0) ; (make-ord (m y) 2 0) 1)) 0))) (if (p x) (if q (f4 y (dn x) (not q)) (f4 y (up x) (not q))) 4))