(COMMENTS
 problems:
  - not confluent
  - average terminates by bounded increase where the bound is also growing
  - quicksort uses destructors and makes use of average 
)
(VAR x y z n m)
(RULES
 average(x,y) -> if(ge(x,y),x,y)
 if(true,x,y) -> averIter(y,x,y)
 if(false,x,y) -> averIter(x,y,x)
 averIter(x,y,z) -> ifIter(ge(x,y),x,y,z)
 ifIter(true,x,y,z) -> z
 ifIter(false,x,y,z) -> averIter(plus(x,s(s(s(0)))),plus(y,s(0)),plus(z,s(0)))

 append(nil,y) -> y
 append(cons(n,x),y) -> cons(n,app(x,y))
 low(n,nil) -> nil
 low(n,cons(m,x)) -> if_low(ge(m,n),n,cons(m,x))
 if_low(false,n,cons(m,x)) -> cons(m,low(n,x))
 if_low(true,n,cons(m,x)) -> low(n,x)
 high(n,nil) -> nil
 high(n,cons(m,x)) -> if_high(ge(m,n),n,cons(m,x))
 if_high(false,n,cons(m,x)) -> high(n,x)
 if_high(true,n,cons(m,x)) -> cons(average(m,m),high(n,x))
 quicksort(x) -> ifquick(isempty(x),x)
 ifquick(true,x) -> nil
 ifquick(false,x) -> append(quicksort(low(head(x),tail(x))), cons(tail(x),quicksort(high(head(x),tail(x)))))

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

 isempty(nil) -> true
 isempty(cons(n,x)) -> false
 head(nil) -> error
 head(cons(n,x)) -> n
 tail(nil) -> nil
 tail(cons(n,x)) -> x
 ge(x,0) -> true
 ge(0,s(y)) -> false
 ge(s(x),s(y)) -> ge(x,y)

 a -> b
 a -> c
)