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

(include-book "ordinals/ordinals" :dir :system)

(defthm lemma-1
  (implies (p x)
           (not (equal 0 (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
                                   (o^ (omega) (m x))
                                 (if (p y)
                                     (o* (o^ (omega) (m y)) 2)
                                   1))
                             0)))
  (if (p x)
      (if q
          (f4 y (dn x) (not q))
        (f4 y (up x) (not q)))
    4))