; 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))