goodstein

(defun pfix
  (x)
  (declare (xargs :guard t))
  (if (and (integerp x) (> x 0))
    x
    1))

(defun ilog-loop
  (nbr base pow l)
  (declare (xargs :guard (and (integerp nbr)
        (> nbr 0)
        (integerp base)
        (> base 1)
        (integerp pow)
        (integerp l)
        (>= l 0))
      :measure (let ((nbr (pfix nbr)) (l (nfix l)))
        (if (>= l nbr)
          0
          (- nbr l)))))
  (let ((nbr (pfix nbr)) (l (nfix l)))
    (if (>= l nbr)
      l
      (if (> pow nbr)
        l
        (ilog-loop nbr base (* base pow) (+ l 1))))))

(defun ilog
  (nbr base)
  "Return Log_base(nbr)."
  (declare (xargs :guard (and (integerp nbr) (> nbr 0) (integerp base) (> base 1))))
  (ilog-loop nbr base base 0))

(defun scalep
  (x n)
  "A Scale of base n is just like an ACL2 representation
   of an ordinal less than epsilon 0 except that the base
   used to transform the representation into an actual
   ordinal is n instead of omega. Thus Scales of base n
   represent nonnegative integers. Therefore, a Scale of base
   n is either a nonnegative integer less than n or of the
   form '(x_1 ... x_j . k) where k is a nonnegative integer
   less than n, none of the x_i's are 0, each of the x_i's
   is a Scale of base n, and the x_i's are listed in
   non-increasing ordinal order."
  (declare (xargs :guard (and (integerp n) (> n 1))))
  (if (consp x)
    (and (scalep (car x) n)
      (not (equal (car x) 0))
      (scalep (cdr x) n)
      (or (atom (cdr x)) (not (e0-ord-< (car x) (cadr x)))))
    (and (integerp x) (>= x 0) (< x n))))

(defun nbr-to-scale
  (nbr base)
  "Convert nbr to a Scale with the given base."
  (declare (xargs :guard (and (integerp nbr) (>= nbr 0) (integerp base) (> base 1))
      :mode :program))
  (if (< nbr base)
    nbr
    (let ((ilog (ilog nbr base)))
      (cons (nbr-to-scale ilog base)
        (nbr-to-scale (- nbr (expt base ilog)) base)))))

(defun e0-ordinalp-to-nbr
  (ord base)
  "Used to convert a Scale, with the given base, to a number."
  (declare (xargs :guard (and (integerp base) (> base 1) (e0-ordinalp ord))
      :verify-guards nil))
  (if (consp ord)
    (+ (expt base (e0-ordinalp-to-nbr (car ord) base))
      (e0-ordinalp-to-nbr (cdr ord) base))
    ord))

(defun goodstein
  (x b)
  (declare (xargs :mode :program))
  (let* ((gn (nbr-to-scale x b)) (y (e0-ordinalp-to-nbr gn (+ b 1))))
    (if (zp x)
      (list (list x b))
      (cons (list x b) (goodstein (- y 1) (+ b 1))))))