YES

Problem:
 app'(app'(minus(),x),0()) -> x
 app'(app'(minus(),app'(s(),x)),app'(s(),y)) -> app'(app'(minus(),x),y)
 app'(app'(quot(),0()),app'(s(),y)) -> 0()
 app'(app'(quot(),app'(s(),x)),app'(s(),y)) ->
 app'(s(),app'(app'(quot(),app'(app'(minus(),x),y)),app'(s(),y)))
 app'(app'(le(),0()),y) -> true()
 app'(app'(le(),app'(s(),x)),0()) -> false()
 app'(app'(le(),app'(s(),x)),app'(s(),y)) -> app'(app'(le(),x),y)
 app'(app'(app(),nil()),y) -> y
 app'(app'(app(),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(app(),x),y))
 app'(app'(low(),n),nil()) -> nil()
 app'(app'(low(),n),app'(app'(add(),m),x)) ->
 app'(app'(app'(if_low(),app'(app'(le(),m),n)),n),app'(app'(add(),m),x))
 app'(app'(app'(if_low(),true()),n),app'(app'(add(),m),x)) ->
 app'(app'(add(),m),app'(app'(low(),n),x))
 app'(app'(app'(if_low(),false()),n),app'(app'(add(),m),x)) -> app'(app'(low(),n),x)
 app'(app'(high(),n),nil()) -> nil()
 app'(app'(high(),n),app'(app'(add(),m),x)) ->
 app'(app'(app'(if_high(),app'(app'(le(),m),n)),n),app'(app'(add(),m),x))
 app'(app'(app'(if_high(),true()),n),app'(app'(add(),m),x)) -> app'(app'(high(),n),x)
 app'(app'(app'(if_high(),false()),n),app'(app'(add(),m),x)) ->
 app'(app'(add(),m),app'(app'(high(),n),x))
 app'(quicksort(),nil()) -> nil()
 app'(quicksort(),app'(app'(add(),n),x)) ->
 app'(app'(app(),app'(quicksort(),app'(app'(low(),n),x))),app'(app'(add(),n),
                                                               app'(quicksort(),
                                                                    app'
                                                                    (app'(high(),n),x))))
 app'(app'(map(),f),nil()) -> nil()
 app'(app'(map(),f),app'(app'(add(),x),xs)) -> app'(app'(add(),app'(f,x)),app'(app'(map(),f),xs))
 app'(app'(filter(),f),nil()) -> nil()
 app'(app'(filter(),f),app'(app'(add(),x),xs)) ->
 app'(app'(app'(app'(filter2(),app'(f,x)),f),x),xs)
 app'(app'(app'(app'(filter2(),true()),f),x),xs) -> app'(app'(add(),x),app'(app'(filter(),f),xs))
 app'(app'(app'(app'(filter2(),false()),f),x),xs) -> app'(app'(filter(),f),xs)

Proof:
 Uncurry Processor:
  minus2(x,0()) -> x
  minus2(s1(x),s1(y)) -> minus2(x,y)
  quot2(0(),s1(y)) -> 0()
  quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
  le2(0(),y) -> true()
  le2(s1(x),0()) -> false()
  le2(s1(x),s1(y)) -> le2(x,y)
  app2(nil(),y) -> y
  app2(add2(n,x),y) -> add2(n,app2(x,y))
  low2(n,nil()) -> nil()
  low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
  if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
  if_low3(false(),n,add2(m,x)) -> low2(n,x)
  high2(n,nil()) -> nil()
  high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
  if_high3(true(),n,add2(m,x)) -> high2(n,x)
  if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
  quicksort1(nil()) -> nil()
  quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
  map2(f,nil()) -> nil()
  map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
  filter2(f,nil()) -> nil()
  filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
  filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
  filter24(false(),f,x,xs) -> filter2(f,xs)
  app'(minus1(x8),x9) -> minus2(x8,x9)
  app'(minus(),x9) -> minus1(x9)
  app'(s(),x9) -> s1(x9)
  app'(quot1(x8),x9) -> quot2(x8,x9)
  app'(quot(),x9) -> quot1(x9)
  app'(le1(x8),x9) -> le2(x8,x9)
  app'(le(),x9) -> le1(x9)
  app'(app1(x8),x9) -> app2(x8,x9)
  app'(app(),x9) -> app1(x9)
  app'(add1(x8),x9) -> add2(x8,x9)
  app'(add(),x9) -> add1(x9)
  app'(low1(x8),x9) -> low2(x8,x9)
  app'(low(),x9) -> low1(x9)
  app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
  app'(if_low1(x8),x9) -> if_low2(x8,x9)
  app'(if_low(),x9) -> if_low1(x9)
  app'(high1(x8),x9) -> high2(x8,x9)
  app'(high(),x9) -> high1(x9)
  app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
  app'(if_high1(x8),x9) -> if_high2(x8,x9)
  app'(if_high(),x9) -> if_high1(x9)
  app'(quicksort(),x9) -> quicksort1(x9)
  app'(map1(x8),x9) -> map2(x8,x9)
  app'(map(),x9) -> map1(x9)
  app'(filter1(x8),x9) -> filter2(x8,x9)
  app'(filter(),x9) -> filter1(x9)
  app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
  app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
  app'(filter21(x8),x9) -> filter22(x8,x9)
  app'(filter2(),x9) -> filter21(x9)
  DP Processor:
   DPs:
    minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
    quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
    quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
    le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
    app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
    low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
    low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
    if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
    if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
    high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
    high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
    if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
    if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
    quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
    quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
    quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
    quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
    quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
    map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs)
    map{2,#}(f,add2(x,xs)) -> app'#(f,x)
    filter{2,#}(f,add2(x,xs)) -> app'#(f,x)
    filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
    filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
    filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
    app'#(minus1(x8),x9) -> minus{2,#}(x8,x9)
    app'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
    app'#(le1(x8),x9) -> le{2,#}(x8,x9)
    app'#(app1(x8),x9) -> app{2,#}(x8,x9)
    app'#(low1(x8),x9) -> low{2,#}(x8,x9)
    app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
    app'#(high1(x8),x9) -> high{2,#}(x8,x9)
    app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
    app'#(quicksort(),x9) -> quicksort{1,#}(x9)
    app'#(map1(x8),x9) -> map{2,#}(x8,x9)
    app'#(filter1(x8),x9) -> filter{2,#}(x8,x9)
    app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
   TRS:
    minus2(x,0()) -> x
    minus2(s1(x),s1(y)) -> minus2(x,y)
    quot2(0(),s1(y)) -> 0()
    quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
    le2(0(),y) -> true()
    le2(s1(x),0()) -> false()
    le2(s1(x),s1(y)) -> le2(x,y)
    app2(nil(),y) -> y
    app2(add2(n,x),y) -> add2(n,app2(x,y))
    low2(n,nil()) -> nil()
    low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
    if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
    if_low3(false(),n,add2(m,x)) -> low2(n,x)
    high2(n,nil()) -> nil()
    high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
    if_high3(true(),n,add2(m,x)) -> high2(n,x)
    if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
    quicksort1(nil()) -> nil()
    quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
    map2(f,nil()) -> nil()
    map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
    filter2(f,nil()) -> nil()
    filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
    filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
    filter24(false(),f,x,xs) -> filter2(f,xs)
    app'(minus1(x8),x9) -> minus2(x8,x9)
    app'(minus(),x9) -> minus1(x9)
    app'(s(),x9) -> s1(x9)
    app'(quot1(x8),x9) -> quot2(x8,x9)
    app'(quot(),x9) -> quot1(x9)
    app'(le1(x8),x9) -> le2(x8,x9)
    app'(le(),x9) -> le1(x9)
    app'(app1(x8),x9) -> app2(x8,x9)
    app'(app(),x9) -> app1(x9)
    app'(add1(x8),x9) -> add2(x8,x9)
    app'(add(),x9) -> add1(x9)
    app'(low1(x8),x9) -> low2(x8,x9)
    app'(low(),x9) -> low1(x9)
    app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
    app'(if_low1(x8),x9) -> if_low2(x8,x9)
    app'(if_low(),x9) -> if_low1(x9)
    app'(high1(x8),x9) -> high2(x8,x9)
    app'(high(),x9) -> high1(x9)
    app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
    app'(if_high1(x8),x9) -> if_high2(x8,x9)
    app'(if_high(),x9) -> if_high1(x9)
    app'(quicksort(),x9) -> quicksort1(x9)
    app'(map1(x8),x9) -> map2(x8,x9)
    app'(map(),x9) -> map1(x9)
    app'(filter1(x8),x9) -> filter2(x8,x9)
    app'(filter(),x9) -> filter1(x9)
    app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
    app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
    app'(filter21(x8),x9) -> filter22(x8,x9)
    app'(filter2(),x9) -> filter21(x9)
   TDG Processor:
    DPs:
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
     low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
     if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
     if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
     high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
     if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
     if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
     quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
     quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
     map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x)
     filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app'#(minus1(x8),x9) -> minus{2,#}(x8,x9)
     app'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
     app'#(le1(x8),x9) -> le{2,#}(x8,x9)
     app'#(app1(x8),x9) -> app{2,#}(x8,x9)
     app'#(low1(x8),x9) -> low{2,#}(x8,x9)
     app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
     app'#(high1(x8),x9) -> high{2,#}(x8,x9)
     app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
     app'#(quicksort(),x9) -> quicksort{1,#}(x9)
     app'#(map1(x8),x9) -> map{2,#}(x8,x9)
     app'#(filter1(x8),x9) -> filter{2,#}(x8,x9)
     app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
    TRS:
     minus2(x,0()) -> x
     minus2(s1(x),s1(y)) -> minus2(x,y)
     quot2(0(),s1(y)) -> 0()
     quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
     le2(0(),y) -> true()
     le2(s1(x),0()) -> false()
     le2(s1(x),s1(y)) -> le2(x,y)
     app2(nil(),y) -> y
     app2(add2(n,x),y) -> add2(n,app2(x,y))
     low2(n,nil()) -> nil()
     low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
     if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
     if_low3(false(),n,add2(m,x)) -> low2(n,x)
     high2(n,nil()) -> nil()
     high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
     if_high3(true(),n,add2(m,x)) -> high2(n,x)
     if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
     quicksort1(nil()) -> nil()
     quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
     map2(f,nil()) -> nil()
     map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app'(minus1(x8),x9) -> minus2(x8,x9)
     app'(minus(),x9) -> minus1(x9)
     app'(s(),x9) -> s1(x9)
     app'(quot1(x8),x9) -> quot2(x8,x9)
     app'(quot(),x9) -> quot1(x9)
     app'(le1(x8),x9) -> le2(x8,x9)
     app'(le(),x9) -> le1(x9)
     app'(app1(x8),x9) -> app2(x8,x9)
     app'(app(),x9) -> app1(x9)
     app'(add1(x8),x9) -> add2(x8,x9)
     app'(add(),x9) -> add1(x9)
     app'(low1(x8),x9) -> low2(x8,x9)
     app'(low(),x9) -> low1(x9)
     app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
     app'(if_low1(x8),x9) -> if_low2(x8,x9)
     app'(if_low(),x9) -> if_low1(x9)
     app'(high1(x8),x9) -> high2(x8,x9)
     app'(high(),x9) -> high1(x9)
     app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
     app'(if_high1(x8),x9) -> if_high2(x8,x9)
     app'(if_high(),x9) -> if_high1(x9)
     app'(quicksort(),x9) -> quicksort1(x9)
     app'(map1(x8),x9) -> map2(x8,x9)
     app'(map(),x9) -> map1(x9)
     app'(filter1(x8),x9) -> filter2(x8,x9)
     app'(filter(),x9) -> filter1(x9)
     app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
     app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
     app'(filter21(x8),x9) -> filter22(x8,x9)
     app'(filter2(),x9) -> filter21(x9)
    graph:
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x)
     filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(filter1(x8),x9) -> filter{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(map1(x8),x9) -> map{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(quicksort(),x9) -> quicksort{1,#}(x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(high1(x8),x9) -> high{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(low1(x8),x9) -> low{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(app1(x8),x9) -> app{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(le1(x8),x9) -> le{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(minus1(x8),x9) -> minus{2,#}(x8,x9)
     app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) ->
     filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) ->
     filter{2,#}(f,add2(x,xs)) -> app'#(f,x)
     app'#(map1(x8),x9) -> map{2,#}(x8,x9) ->
     map{2,#}(f,add2(x,xs)) -> app'#(f,x)
     app'#(map1(x8),x9) -> map{2,#}(x8,x9) ->
     map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs)
     app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9) ->
     if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
     app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9) ->
     if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
     app'#(high1(x8),x9) -> high{2,#}(x8,x9) ->
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
     app'#(high1(x8),x9) -> high{2,#}(x8,x9) ->
     high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9) ->
     if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
     app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9) ->
     if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
     app'#(low1(x8),x9) -> low{2,#}(x8,x9) ->
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
     app'#(low1(x8),x9) -> low{2,#}(x8,x9) ->
     low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     app'#(app1(x8),x9) -> app{2,#}(x8,x9) ->
     app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
     app'#(le1(x8),x9) -> le{2,#}(x8,x9) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     app'#(quot1(x8),x9) -> quot{2,#}(x8,x9) ->
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
     app'#(quot1(x8),x9) -> quot{2,#}(x8,x9) ->
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     app'#(minus1(x8),x9) -> minus{2,#}(x8,x9) ->
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
     quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
     app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
     app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
     quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
     app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
     app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
     quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(filter1(x8),x9) -> filter{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(map1(x8),x9) -> map{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(quicksort(),x9) -> quicksort{1,#}(x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(high1(x8),x9) -> high{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(low1(x8),x9) -> low{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(app1(x8),x9) -> app{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(le1(x8),x9) -> le{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
     app'#(minus1(x8),x9) -> minus{2,#}(x8,x9)
     map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,add2(x,xs)) -> app'#(f,x)
     map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs)
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
     quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
     quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
     quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x) ->
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
     quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x) ->
     high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x) ->
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
     quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x) ->
     low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x)))) ->
     app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
     if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x) ->
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
     if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x) ->
     high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x) ->
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
     if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x) ->
     high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x)) ->
     if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
     high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x)) ->
     if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
     high{2,#}(n,add2(m,x)) -> le{2,#}(m,n) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x) ->
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
     if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x) ->
     low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x) ->
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
     if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x) ->
     low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x)) ->
     if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
     low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x)) ->
     if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
     low{2,#}(n,add2(m,x)) -> le{2,#}(m,n) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     app{2,#}(add2(n,x),y) -> app{2,#}(x,y) ->
     app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y)) ->
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y)) ->
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) -> minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
    SCC Processor:
     #sccs: 8
     #rules: 21
     #arcs: 91/1296
     DPs:
      filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
      filter{2,#}(f,add2(x,xs)) -> app'#(f,x)
      app'#(map1(x8),x9) -> map{2,#}(x8,x9)
      map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs)
      map{2,#}(f,add2(x,xs)) -> app'#(f,x)
      app'#(filter1(x8),x9) -> filter{2,#}(x8,x9)
      filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
      filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
      app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 1
       pi(app'#) = 1
       pi(filter{2,#}) = 1
       pi(filter2{4,#}) = 3
      problem:
       DPs:
        filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
        app'#(map1(x8),x9) -> map{2,#}(x8,x9)
        app'#(filter1(x8),x9) -> filter{2,#}(x8,x9)
        filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
        app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        app2(nil(),y) -> y
        app2(add2(n,x),y) -> add2(n,app2(x,y))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        quicksort1(nil()) -> nil()
        quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
        map2(f,nil()) -> nil()
        map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x8),x9) -> minus2(x8,x9)
        app'(minus(),x9) -> minus1(x9)
        app'(s(),x9) -> s1(x9)
        app'(quot1(x8),x9) -> quot2(x8,x9)
        app'(quot(),x9) -> quot1(x9)
        app'(le1(x8),x9) -> le2(x8,x9)
        app'(le(),x9) -> le1(x9)
        app'(app1(x8),x9) -> app2(x8,x9)
        app'(app(),x9) -> app1(x9)
        app'(add1(x8),x9) -> add2(x8,x9)
        app'(add(),x9) -> add1(x9)
        app'(low1(x8),x9) -> low2(x8,x9)
        app'(low(),x9) -> low1(x9)
        app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
        app'(if_low1(x8),x9) -> if_low2(x8,x9)
        app'(if_low(),x9) -> if_low1(x9)
        app'(high1(x8),x9) -> high2(x8,x9)
        app'(high(),x9) -> high1(x9)
        app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
        app'(if_high1(x8),x9) -> if_high2(x8,x9)
        app'(if_high(),x9) -> if_high1(x9)
        app'(quicksort(),x9) -> quicksort1(x9)
        app'(map1(x8),x9) -> map2(x8,x9)
        app'(map(),x9) -> map1(x9)
        app'(filter1(x8),x9) -> filter2(x8,x9)
        app'(filter(),x9) -> filter1(x9)
        app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app'(filter21(x8),x9) -> filter22(x8,x9)
        app'(filter2(),x9) -> filter21(x9)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 20/25
       
     
     DPs:
      quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
      quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Usable Rule Processor:
      DPs:
       quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
       quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
      TRS:
       high2(n,nil()) -> nil()
       high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
       if_high3(true(),n,add2(m,x)) -> high2(n,x)
       if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
       le2(0(),y) -> true()
       le2(s1(x),0()) -> false()
       le2(s1(x),s1(y)) -> le2(x,y)
       low2(n,nil()) -> nil()
       low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
       if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
       if_low3(false(),n,add2(m,x)) -> low2(n,x)
      KBO Processor:
       argument filtering:
        pi(0) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
        pi(s1) = 0
        pi(le2) = 1
        pi(add2) = [1]
        pi(low2) = 1
        pi(if_low3) = 2
        pi(high2) = 1
        pi(if_high3) = 2
        pi(quicksort{1,#}) = [0]
       usable rules:
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
       weight function:
        w0 = 1
        w(quicksort{1,#}) = w(if_high3) = w(if_low3) = w(nil) = w(false) = w(
        true) = w(0) = 1
        w(high2) = w(low2) = w(add2) = w(le2) = w(s1) = 0
       precedence:
        quicksort{1,#} ~ if_high3 ~ high2 ~ if_low3 ~ low2 ~ add2 ~ le2 ~ 
        s1 ~ nil ~ false ~ true ~ 0
       problem:
        DPs:
         
        TRS:
         high2(n,nil()) -> nil()
         high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
         if_high3(true(),n,add2(m,x)) -> high2(n,x)
         if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
         le2(0(),y) -> true()
         le2(s1(x),0()) -> false()
         le2(s1(x),s1(y)) -> le2(x,y)
         low2(n,nil()) -> nil()
         low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
         if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
         if_low3(false(),n,add2(m,x)) -> low2(n,x)
       Qed
     
     DPs:
      high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
      if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
      if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(high{2,#}) = 1
       pi(if_high{3,#}) = 2
      problem:
       DPs:
        high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        app2(nil(),y) -> y
        app2(add2(n,x),y) -> add2(n,app2(x,y))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        quicksort1(nil()) -> nil()
        quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
        map2(f,nil()) -> nil()
        map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x8),x9) -> minus2(x8,x9)
        app'(minus(),x9) -> minus1(x9)
        app'(s(),x9) -> s1(x9)
        app'(quot1(x8),x9) -> quot2(x8,x9)
        app'(quot(),x9) -> quot1(x9)
        app'(le1(x8),x9) -> le2(x8,x9)
        app'(le(),x9) -> le1(x9)
        app'(app1(x8),x9) -> app2(x8,x9)
        app'(app(),x9) -> app1(x9)
        app'(add1(x8),x9) -> add2(x8,x9)
        app'(add(),x9) -> add1(x9)
        app'(low1(x8),x9) -> low2(x8,x9)
        app'(low(),x9) -> low1(x9)
        app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
        app'(if_low1(x8),x9) -> if_low2(x8,x9)
        app'(if_low(),x9) -> if_low1(x9)
        app'(high1(x8),x9) -> high2(x8,x9)
        app'(high(),x9) -> high1(x9)
        app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
        app'(if_high1(x8),x9) -> if_high2(x8,x9)
        app'(if_high(),x9) -> if_high1(x9)
        app'(quicksort(),x9) -> quicksort1(x9)
        app'(map1(x8),x9) -> map2(x8,x9)
        app'(map(),x9) -> map1(x9)
        app'(filter1(x8),x9) -> filter2(x8,x9)
        app'(filter(),x9) -> filter1(x9)
        app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app'(filter21(x8),x9) -> filter22(x8,x9)
        app'(filter2(),x9) -> filter21(x9)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 4/1
       
     
     DPs:
      low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
      if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
      if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(low{2,#}) = 1
       pi(if_low{3,#}) = 2
      problem:
       DPs:
        low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        app2(nil(),y) -> y
        app2(add2(n,x),y) -> add2(n,app2(x,y))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        quicksort1(nil()) -> nil()
        quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
        map2(f,nil()) -> nil()
        map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x8),x9) -> minus2(x8,x9)
        app'(minus(),x9) -> minus1(x9)
        app'(s(),x9) -> s1(x9)
        app'(quot1(x8),x9) -> quot2(x8,x9)
        app'(quot(),x9) -> quot1(x9)
        app'(le1(x8),x9) -> le2(x8,x9)
        app'(le(),x9) -> le1(x9)
        app'(app1(x8),x9) -> app2(x8,x9)
        app'(app(),x9) -> app1(x9)
        app'(add1(x8),x9) -> add2(x8,x9)
        app'(add(),x9) -> add1(x9)
        app'(low1(x8),x9) -> low2(x8,x9)
        app'(low(),x9) -> low1(x9)
        app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
        app'(if_low1(x8),x9) -> if_low2(x8,x9)
        app'(if_low(),x9) -> if_low1(x9)
        app'(high1(x8),x9) -> high2(x8,x9)
        app'(high(),x9) -> high1(x9)
        app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
        app'(if_high1(x8),x9) -> if_high2(x8,x9)
        app'(if_high(),x9) -> if_high1(x9)
        app'(quicksort(),x9) -> quicksort1(x9)
        app'(map1(x8),x9) -> map2(x8,x9)
        app'(map(),x9) -> map1(x9)
        app'(filter1(x8),x9) -> filter2(x8,x9)
        app'(filter(),x9) -> filter1(x9)
        app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app'(filter21(x8),x9) -> filter22(x8,x9)
        app'(filter2(),x9) -> filter21(x9)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 4/1
       
     
     DPs:
      app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(app{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        app2(nil(),y) -> y
        app2(add2(n,x),y) -> add2(n,app2(x,y))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        quicksort1(nil()) -> nil()
        quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
        map2(f,nil()) -> nil()
        map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x8),x9) -> minus2(x8,x9)
        app'(minus(),x9) -> minus1(x9)
        app'(s(),x9) -> s1(x9)
        app'(quot1(x8),x9) -> quot2(x8,x9)
        app'(quot(),x9) -> quot1(x9)
        app'(le1(x8),x9) -> le2(x8,x9)
        app'(le(),x9) -> le1(x9)
        app'(app1(x8),x9) -> app2(x8,x9)
        app'(app(),x9) -> app1(x9)
        app'(add1(x8),x9) -> add2(x8,x9)
        app'(add(),x9) -> add1(x9)
        app'(low1(x8),x9) -> low2(x8,x9)
        app'(low(),x9) -> low1(x9)
        app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
        app'(if_low1(x8),x9) -> if_low2(x8,x9)
        app'(if_low(),x9) -> if_low1(x9)
        app'(high1(x8),x9) -> high2(x8,x9)
        app'(high(),x9) -> high1(x9)
        app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
        app'(if_high1(x8),x9) -> if_high2(x8,x9)
        app'(if_high(),x9) -> if_high1(x9)
        app'(quicksort(),x9) -> quicksort1(x9)
        app'(map1(x8),x9) -> map2(x8,x9)
        app'(map(),x9) -> map1(x9)
        app'(filter1(x8),x9) -> filter2(x8,x9)
        app'(filter(),x9) -> filter1(x9)
        app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app'(filter21(x8),x9) -> filter22(x8,x9)
        app'(filter2(),x9) -> filter21(x9)
      Qed
     
     DPs:
      le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(le{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        app2(nil(),y) -> y
        app2(add2(n,x),y) -> add2(n,app2(x,y))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        quicksort1(nil()) -> nil()
        quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
        map2(f,nil()) -> nil()
        map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x8),x9) -> minus2(x8,x9)
        app'(minus(),x9) -> minus1(x9)
        app'(s(),x9) -> s1(x9)
        app'(quot1(x8),x9) -> quot2(x8,x9)
        app'(quot(),x9) -> quot1(x9)
        app'(le1(x8),x9) -> le2(x8,x9)
        app'(le(),x9) -> le1(x9)
        app'(app1(x8),x9) -> app2(x8,x9)
        app'(app(),x9) -> app1(x9)
        app'(add1(x8),x9) -> add2(x8,x9)
        app'(add(),x9) -> add1(x9)
        app'(low1(x8),x9) -> low2(x8,x9)
        app'(low(),x9) -> low1(x9)
        app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
        app'(if_low1(x8),x9) -> if_low2(x8,x9)
        app'(if_low(),x9) -> if_low1(x9)
        app'(high1(x8),x9) -> high2(x8,x9)
        app'(high(),x9) -> high1(x9)
        app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
        app'(if_high1(x8),x9) -> if_high2(x8,x9)
        app'(if_high(),x9) -> if_high1(x9)
        app'(quicksort(),x9) -> quicksort1(x9)
        app'(map1(x8),x9) -> map2(x8,x9)
        app'(map(),x9) -> map1(x9)
        app'(filter1(x8),x9) -> filter2(x8,x9)
        app'(filter(),x9) -> filter1(x9)
        app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app'(filter21(x8),x9) -> filter22(x8,x9)
        app'(filter2(),x9) -> filter21(x9)
      Qed
     
     DPs:
      quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Usable Rule Processor:
      DPs:
       quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
      TRS:
       minus2(x,0()) -> x
       minus2(s1(x),s1(y)) -> minus2(x,y)
      Arctic Interpretation Processor:
       dimension: 1
       usable rules:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
       interpretation:
        [quot{2,#}](x0, x1) = 3x0 + -16,
        
        [s1](x0) = 1x0 + -3,
        
        [minus2](x0, x1) = x0 + -11,
        
        [0] = 8
       orientation:
        quot{2,#}(s1(x),s1(y)) = 4x + 0 >= 3x + -8 = quot{2,#}(minus2(x,y),s1(y))
        
        minus2(x,0()) = x + -11 >= x = x
        
        minus2(s1(x),s1(y)) = 1x + -3 >= x + -11 = minus2(x,y)
       problem:
        DPs:
         
        TRS:
         minus2(x,0()) -> x
         minus2(s1(x),s1(y)) -> minus2(x,y)
       Qed
     
     DPs:
      minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      app2(nil(),y) -> y
      app2(add2(n,x),y) -> add2(n,app2(x,y))
      low2(n,nil()) -> nil()
      low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
      if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
      if_low3(false(),n,add2(m,x)) -> low2(n,x)
      high2(n,nil()) -> nil()
      high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
      if_high3(true(),n,add2(m,x)) -> high2(n,x)
      if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
      quicksort1(nil()) -> nil()
      quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
      map2(f,nil()) -> nil()
      map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x8),x9) -> minus2(x8,x9)
      app'(minus(),x9) -> minus1(x9)
      app'(s(),x9) -> s1(x9)
      app'(quot1(x8),x9) -> quot2(x8,x9)
      app'(quot(),x9) -> quot1(x9)
      app'(le1(x8),x9) -> le2(x8,x9)
      app'(le(),x9) -> le1(x9)
      app'(app1(x8),x9) -> app2(x8,x9)
      app'(app(),x9) -> app1(x9)
      app'(add1(x8),x9) -> add2(x8,x9)
      app'(add(),x9) -> add1(x9)
      app'(low1(x8),x9) -> low2(x8,x9)
      app'(low(),x9) -> low1(x9)
      app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
      app'(if_low1(x8),x9) -> if_low2(x8,x9)
      app'(if_low(),x9) -> if_low1(x9)
      app'(high1(x8),x9) -> high2(x8,x9)
      app'(high(),x9) -> high1(x9)
      app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
      app'(if_high1(x8),x9) -> if_high2(x8,x9)
      app'(if_high(),x9) -> if_high1(x9)
      app'(quicksort(),x9) -> quicksort1(x9)
      app'(map1(x8),x9) -> map2(x8,x9)
      app'(map(),x9) -> map1(x9)
      app'(filter1(x8),x9) -> filter2(x8,x9)
      app'(filter(),x9) -> filter1(x9)
      app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app'(filter21(x8),x9) -> filter22(x8,x9)
      app'(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(minus{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        app2(nil(),y) -> y
        app2(add2(n,x),y) -> add2(n,app2(x,y))
        low2(n,nil()) -> nil()
        low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
        if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
        if_low3(false(),n,add2(m,x)) -> low2(n,x)
        high2(n,nil()) -> nil()
        high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
        if_high3(true(),n,add2(m,x)) -> high2(n,x)
        if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
        quicksort1(nil()) -> nil()
        quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
        map2(f,nil()) -> nil()
        map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> add2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x8),x9) -> minus2(x8,x9)
        app'(minus(),x9) -> minus1(x9)
        app'(s(),x9) -> s1(x9)
        app'(quot1(x8),x9) -> quot2(x8,x9)
        app'(quot(),x9) -> quot1(x9)
        app'(le1(x8),x9) -> le2(x8,x9)
        app'(le(),x9) -> le1(x9)
        app'(app1(x8),x9) -> app2(x8,x9)
        app'(app(),x9) -> app1(x9)
        app'(add1(x8),x9) -> add2(x8,x9)
        app'(add(),x9) -> add1(x9)
        app'(low1(x8),x9) -> low2(x8,x9)
        app'(low(),x9) -> low1(x9)
        app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
        app'(if_low1(x8),x9) -> if_low2(x8,x9)
        app'(if_low(),x9) -> if_low1(x9)
        app'(high1(x8),x9) -> high2(x8,x9)
        app'(high(),x9) -> high1(x9)
        app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
        app'(if_high1(x8),x9) -> if_high2(x8,x9)
        app'(if_high(),x9) -> if_high1(x9)
        app'(quicksort(),x9) -> quicksort1(x9)
        app'(map1(x8),x9) -> map2(x8,x9)
        app'(map(),x9) -> map1(x9)
        app'(filter1(x8),x9) -> filter2(x8,x9)
        app'(filter(),x9) -> filter1(x9)
        app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app'(filter21(x8),x9) -> filter22(x8,x9)
        app'(filter2(),x9) -> filter21(x9)
      Qed