MAYBE

Problem:
 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()

Proof:
 DP Processor:
  DPs:
   average#(x,y) -> ge#(x,y)
   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) -> ge#(x,y)
   averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
   ifIter#(false(),x,y,z) -> plus#(z,s(0()))
   ifIter#(false(),x,y,z) -> plus#(y,s(0()))
   ifIter#(false(),x,y,z) -> plus#(x,s(s(s(0()))))
   ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
   low#(n,cons(m,x)) -> ge#(m,n)
   low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
   if_low#(false(),n,cons(m,x)) -> low#(n,x)
   if_low#(true(),n,cons(m,x)) -> low#(n,x)
   high#(n,cons(m,x)) -> ge#(m,n)
   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)) -> high#(n,x)
   if_high#(true(),n,cons(m,x)) -> average#(m,m)
   quicksort#(x) -> isempty#(x)
   quicksort#(x) -> ifquick#(isempty(x),x)
   ifquick#(false(),x) -> high#(head(x),tail(x))
   ifquick#(false(),x) -> quicksort#(high(head(x),tail(x)))
   ifquick#(false(),x) -> tail#(x)
   ifquick#(false(),x) -> head#(x)
   ifquick#(false(),x) -> low#(head(x),tail(x))
   ifquick#(false(),x) -> quicksort#(low(head(x),tail(x)))
   ifquick#(false(),x) ->
   append#(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
   plus#(s(x),y) -> plus#(x,y)
   ge#(s(x),s(y)) -> ge#(x,y)
  TRS:
   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()
  Usable Rule Processor:
   DPs:
    average#(x,y) -> ge#(x,y)
    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) -> ge#(x,y)
    averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
    ifIter#(false(),x,y,z) -> plus#(z,s(0()))
    ifIter#(false(),x,y,z) -> plus#(y,s(0()))
    ifIter#(false(),x,y,z) -> plus#(x,s(s(s(0()))))
    ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
    low#(n,cons(m,x)) -> ge#(m,n)
    low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
    if_low#(false(),n,cons(m,x)) -> low#(n,x)
    if_low#(true(),n,cons(m,x)) -> low#(n,x)
    high#(n,cons(m,x)) -> ge#(m,n)
    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)) -> high#(n,x)
    if_high#(true(),n,cons(m,x)) -> average#(m,m)
    quicksort#(x) -> isempty#(x)
    quicksort#(x) -> ifquick#(isempty(x),x)
    ifquick#(false(),x) -> high#(head(x),tail(x))
    ifquick#(false(),x) -> quicksort#(high(head(x),tail(x)))
    ifquick#(false(),x) -> tail#(x)
    ifquick#(false(),x) -> head#(x)
    ifquick#(false(),x) -> low#(head(x),tail(x))
    ifquick#(false(),x) -> quicksort#(low(head(x),tail(x)))
    ifquick#(false(),x) ->
    append#(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
    plus#(s(x),y) -> plus#(x,y)
    ge#(s(x),s(y)) -> ge#(x,y)
   TRS:
    f44(x,y) -> x
    f44(x,y) -> y
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    isempty(nil()) -> true()
    isempty(cons(n,x)) -> false()
    tail(nil()) -> nil()
    tail(cons(n,x)) -> x
    head(nil()) -> error()
    head(cons(n,x)) -> n
    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))
    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())))
    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)
    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)))))
    append(nil(),y) -> y
    append(cons(n,x),y) -> cons(n,app(x,y))
   TDG Processor:
    DPs:
     average#(x,y) -> ge#(x,y)
     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) -> ge#(x,y)
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
     ifIter#(false(),x,y,z) -> plus#(z,s(0()))
     ifIter#(false(),x,y,z) -> plus#(y,s(0()))
     ifIter#(false(),x,y,z) -> plus#(x,s(s(s(0()))))
     ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
     low#(n,cons(m,x)) -> ge#(m,n)
     low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
     if_low#(false(),n,cons(m,x)) -> low#(n,x)
     if_low#(true(),n,cons(m,x)) -> low#(n,x)
     high#(n,cons(m,x)) -> ge#(m,n)
     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)) -> high#(n,x)
     if_high#(true(),n,cons(m,x)) -> average#(m,m)
     quicksort#(x) -> isempty#(x)
     quicksort#(x) -> ifquick#(isempty(x),x)
     ifquick#(false(),x) -> high#(head(x),tail(x))
     ifquick#(false(),x) -> quicksort#(high(head(x),tail(x)))
     ifquick#(false(),x) -> tail#(x)
     ifquick#(false(),x) -> head#(x)
     ifquick#(false(),x) -> low#(head(x),tail(x))
     ifquick#(false(),x) -> quicksort#(low(head(x),tail(x)))
     ifquick#(false(),x) ->
     append#(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
     plus#(s(x),y) -> plus#(x,y)
     ge#(s(x),s(y)) -> ge#(x,y)
    TRS:
     f44(x,y) -> x
     f44(x,y) -> y
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     isempty(nil()) -> true()
     isempty(cons(n,x)) -> false()
     tail(nil()) -> nil()
     tail(cons(n,x)) -> x
     head(nil()) -> error()
     head(cons(n,x)) -> n
     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))
     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())))
     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)
     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)))))
     append(nil(),y) -> y
     append(cons(n,x),y) -> cons(n,app(x,y))
    graph:
     ifquick#(false(),x) -> quicksort#(high(head(x),tail(x))) ->
     quicksort#(x) -> ifquick#(isempty(x),x)
     ifquick#(false(),x) -> quicksort#(high(head(x),tail(x))) ->
     quicksort#(x) -> isempty#(x)
     ifquick#(false(),x) -> quicksort#(low(head(x),tail(x))) ->
     quicksort#(x) -> ifquick#(isempty(x),x)
     ifquick#(false(),x) -> quicksort#(low(head(x),tail(x))) ->
     quicksort#(x) -> isempty#(x)
     ifquick#(false(),x) -> high#(head(x),tail(x)) ->
     high#(n,cons(m,x)) -> if_high#(ge(m,n),n,cons(m,x))
     ifquick#(false(),x) -> high#(head(x),tail(x)) ->
     high#(n,cons(m,x)) -> ge#(m,n)
     ifquick#(false(),x) -> low#(head(x),tail(x)) ->
     low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
     ifquick#(false(),x) -> low#(head(x),tail(x)) ->
     low#(n,cons(m,x)) -> ge#(m,n)
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) ->
     append#(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) -> quicksort#(low(head(x),tail(x)))
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) -> low#(head(x),tail(x))
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) -> head#(x)
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) -> tail#(x)
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) -> quicksort#(high(head(x),tail(x)))
     quicksort#(x) -> ifquick#(isempty(x),x) ->
     ifquick#(false(),x) -> high#(head(x),tail(x))
     if_high#(false(),n,cons(m,x)) -> high#(n,x) ->
     high#(n,cons(m,x)) -> if_high#(ge(m,n),n,cons(m,x))
     if_high#(false(),n,cons(m,x)) -> high#(n,x) ->
     high#(n,cons(m,x)) -> ge#(m,n)
     if_high#(true(),n,cons(m,x)) -> high#(n,x) ->
     high#(n,cons(m,x)) -> if_high#(ge(m,n),n,cons(m,x))
     if_high#(true(),n,cons(m,x)) -> high#(n,x) ->
     high#(n,cons(m,x)) -> ge#(m,n)
     if_high#(true(),n,cons(m,x)) -> average#(m,m) ->
     average#(x,y) -> if#(ge(x,y),x,y)
     if_high#(true(),n,cons(m,x)) -> average#(m,m) ->
     average#(x,y) -> ge#(x,y)
     high#(n,cons(m,x)) -> if_high#(ge(m,n),n,cons(m,x)) ->
     if_high#(true(),n,cons(m,x)) -> average#(m,m)
     high#(n,cons(m,x)) -> if_high#(ge(m,n),n,cons(m,x)) ->
     if_high#(true(),n,cons(m,x)) -> high#(n,x)
     high#(n,cons(m,x)) -> if_high#(ge(m,n),n,cons(m,x)) ->
     if_high#(false(),n,cons(m,x)) -> high#(n,x)
     high#(n,cons(m,x)) -> ge#(m,n) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     if_low#(false(),n,cons(m,x)) -> low#(n,x) ->
     low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
     if_low#(false(),n,cons(m,x)) -> low#(n,x) ->
     low#(n,cons(m,x)) -> ge#(m,n)
     if_low#(true(),n,cons(m,x)) -> low#(n,x) ->
     low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
     if_low#(true(),n,cons(m,x)) -> low#(n,x) ->
     low#(n,cons(m,x)) -> ge#(m,n)
     low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x)) ->
     if_low#(true(),n,cons(m,x)) -> low#(n,x)
     low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x)) ->
     if_low#(false(),n,cons(m,x)) -> low#(n,x)
     low#(n,cons(m,x)) -> ge#(m,n) -> ge#(s(x),s(y)) -> ge#(x,y)
     plus#(s(x),y) -> plus#(x,y) ->
     plus#(s(x),y) -> plus#(x,y)
     ifIter#(false(),x,y,z) -> plus#(z,s(0())) ->
     plus#(s(x),y) -> plus#(x,y)
     ifIter#(false(),x,y,z) -> plus#(y,s(0())) ->
     plus#(s(x),y) -> plus#(x,y)
     ifIter#(false(),x,y,z) -> plus#(x,s(s(s(0())))) ->
     plus#(s(x),y) -> plus#(x,y)
     ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0()))) ->
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
     ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0()))) ->
     averIter#(x,y,z) -> ge#(x,y)
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z) ->
     ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z) ->
     ifIter#(false(),x,y,z) -> plus#(x,s(s(s(0()))))
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z) ->
     ifIter#(false(),x,y,z) -> plus#(y,s(0()))
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z) ->
     ifIter#(false(),x,y,z) -> plus#(z,s(0()))
     averIter#(x,y,z) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y)
     if#(false(),x,y) -> averIter#(x,y,x) ->
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
     if#(false(),x,y) -> averIter#(x,y,x) ->
     averIter#(x,y,z) -> ge#(x,y)
     if#(true(),x,y) -> averIter#(y,x,y) ->
     averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
     if#(true(),x,y) -> averIter#(y,x,y) -> averIter#(x,y,z) -> ge#(x,y)
     ge#(s(x),s(y)) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y)
     average#(x,y) -> if#(ge(x,y),x,y) ->
     if#(false(),x,y) -> averIter#(x,y,x)
     average#(x,y) -> if#(ge(x,y),x,y) ->
     if#(true(),x,y) -> averIter#(y,x,y)
     average#(x,y) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y)
    Restore Modifier:
     DPs:
      average#(x,y) -> ge#(x,y)
      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) -> ge#(x,y)
      averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
      ifIter#(false(),x,y,z) -> plus#(z,s(0()))
      ifIter#(false(),x,y,z) -> plus#(y,s(0()))
      ifIter#(false(),x,y,z) -> plus#(x,s(s(s(0()))))
      ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
      low#(n,cons(m,x)) -> ge#(m,n)
      low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
      if_low#(false(),n,cons(m,x)) -> low#(n,x)
      if_low#(true(),n,cons(m,x)) -> low#(n,x)
      high#(n,cons(m,x)) -> ge#(m,n)
      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)) -> high#(n,x)
      if_high#(true(),n,cons(m,x)) -> average#(m,m)
      quicksort#(x) -> isempty#(x)
      quicksort#(x) -> ifquick#(isempty(x),x)
      ifquick#(false(),x) -> high#(head(x),tail(x))
      ifquick#(false(),x) -> quicksort#(high(head(x),tail(x)))
      ifquick#(false(),x) -> tail#(x)
      ifquick#(false(),x) -> head#(x)
      ifquick#(false(),x) -> low#(head(x),tail(x))
      ifquick#(false(),x) -> quicksort#(low(head(x),tail(x)))
      ifquick#(false(),x) ->
      append#(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
      plus#(s(x),y) -> plus#(x,y)
      ge#(s(x),s(y)) -> ge#(x,y)
     TRS:
      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()
     SCC Processor:
      #sccs: 6
      #rules: 13
      #arcs: 51/900
      DPs:
       ifquick#(false(),x) -> quicksort#(high(head(x),tail(x)))
       quicksort#(x) -> ifquick#(isempty(x),x)
       ifquick#(false(),x) -> quicksort#(low(head(x),tail(x)))
      TRS:
       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()
      Open
      
      DPs:
       low#(n,cons(m,x)) -> if_low#(ge(m,n),n,cons(m,x))
       if_low#(false(),n,cons(m,x)) -> low#(n,x)
       if_low#(true(),n,cons(m,x)) -> low#(n,x)
      TRS:
       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()
      Open
      
      DPs:
       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)) -> high#(n,x)
      TRS:
       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()
      Open
      
      DPs:
       averIter#(x,y,z) -> ifIter#(ge(x,y),x,y,z)
       ifIter#(false(),x,y,z) -> averIter#(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
      TRS:
       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()
      Open
      
      DPs:
       plus#(s(x),y) -> plus#(x,y)
      TRS:
       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()
      Open
      
      DPs:
       ge#(s(x),s(y)) -> ge#(x,y)
      TRS:
       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()
      Open