#|

Challenge problem 2.

This challenge problem involves the "weird" function we discussed in
class.

Here is the definition. We turned off testing since running weird can
take a long time.

|#

(acl2s-defaults :set testing-enabled nil)

(definec weird (x :nat y :nat) :pos
  :skip-tests t
  (cond ((equal x 0) (+ 1 y))
        ((equal y 0) (weird (- x 1) 1))
        (t (weird (- x 1) (weird x (- y 1))))))

; Try this to see how long that even on small values weird takes a
; long time.
(time$ (weird 4 1))


#|

To get 1000 exam points (a guaranteed A in the course), define a
program that can successfully compute and print out the value of

(weird 4 4)

The program can be in any language you want and it only needs to be
equivalent to the above definition, eg, it does not have to recur the
way the above definition recurs. It doesn't even have to be able to
compute anything but (weird 4 4). The answer has to be a
binary/decimal number.

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

Warning: don't expect to be able to do this, but trying is a useful
exercise.

|#