(COMMENT
 prod([x1,..,xn]) computes the product of the xi's.

 problems:
  - times terminates by bounded increase
  - prod uses destructors, and times is used inside recursive call
  - not confluent

)
(VAR x y z u xs)
(RULES
 prod(xs) -> prodIter(xs,s(0))
 prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
 ifProd(true,xs,x) -> x
 ifProd(false,xs,x) -> prodIter(tail(xs),times(x,head(xs)))

 plus(0,y) -> y
 plus(s(x),y) -> s(plus(x,y))

 times(x,y) -> timesIter(x,y,0,0)
 timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
 ifTimes(true,x,y,z,u) -> z
 ifTimes(false,x,y,z,u) -> timesIter(x,y,plus(y,z),s(u)) 
 
 isempty(nil) -> true
 isempty(cons(x,xs)) -> false
 head(nil) -> error
 head(cons(x,xs)) -> x
 tail(nil) -> nil
 tail(cons(x,xs)) -> xs

 ge(x,0) -> true
 ge(0,s(y)) -> false
 ge(s(x),s(y)) -> ge(x,y)

 a -> b
 a -> c
)