#|

Challenge problem 3.

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

ACL2s proves that weird terminates as you can see below.  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))))))


#|

To get 400 homework points (that is credit for 4 homeworks), prove
that weird terminates using measure functions as described in the
lecture notes. If you don't need all 400 points to get a 100 on your
homeworks, then we'll convert these points into you corresponding
quiz/exam points (1 homework point is not not 1 exam point!).

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.

|#