#|

Challenge problem 5.

This challenge problem involves determining if the following function
is terminating.

|#

(defdata foo-expr (oneof symbol (list foo-expr 'foo foo-expr foo-expr)))

(definec foo-expand (x :foo-expr) :foo-expr
  (if (symbolp x)
      x
    (let ((arg1 (car x))
          (arg3 (third x))
          (arg4 (fourth x)))
      (if (symbolp arg1)
          `(,arg1 foo ,(foo-expand arg3) ,(foo-expand arg4))
        (foo-expand `(,(second arg1)
                      foo
                      (,(third arg1) foo ,arg3 ,arg4)
                      (,(fourth arg1) foo ,arg3 ,arg4)))))))

#|

To get 100 homework points (that is credit for 1 homework), 
determine if the function is terminating.

1. If it is terminating, then prove it by coming up with an
   appropriate measure function and proving termination.

2. If it is not terminating, then provide an input for which
   foo-expand runs forever.

You have to work individually, by yourselves (no partners) and cannot
use any external sources for help.

Submit your solution to me for extra credit.

No partial credit will be given.

|#