#|

Challenge problem 4.

This challenge problem involves the collatz function we discussed in
class.

Here is the definition.

|#

(acl2s-defaults :set testing-enabled nil)

:program
(definec c (n :nat) :nat
  :skip-tests t
  (cond ((< n 2) n)
        ((evenp n) (c (/ n 2)))
        (t (c (+ 1 (* 3 n))))))



"
The following function shows the sequence of numbers that c gets called on.
"

(definec c-list (n :nat) :tl
  (cond ((< n 2) (list n))
        ((integerp (/ n 2))
         (cons n (c-list (/ n 2))))
        (t (cons n (c-list (+ 1 (* 3 n)))))))

" 
The next function returns a list whose first element is the length
of the sequence of numbers c gets called on, and whose second element
is the sequence.

"
(definec c-list-len (n :nat) :all
  (let ((res (c-list n)))
    (list (len res) res)))

#|

To get 100 homework points (that is credit for 1 homework), write code
that determines the smallest natural number > 2,000,000,000 for which
c takes strictly more steps to terminate than any other smaller
number.

You have to work by yourselves on this and cannot use any external
sources for help.

You can write your code in any language. Submit your code and the
answer to me for extra credit.

|#