MAYBE

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)
     Open
     
     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)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [quot{2,#}](x0, x1) = x0,
       
       [filter21](x0) = 4x0 + 2,
       
       [filter22](x0, x1) = 3,
       
       [filter24](x0, x1, x2, x3) = 0,
       
       [filter23](x0, x1, x2) = x2,
       
       [filter2](x0, x1) = 0,
       
       [filter1](x0) = 2,
       
       [map2](x0, x1) = x0 + 4x1 + 6,
       
       [map1](x0) = 4x0 + 3,
       
       [quicksort1](x0) = 0,
       
       [if_high1](x0) = 4,
       
       [if_high3](x0, x1, x2) = 4x2,
       
       [if_high2](x0, x1) = 2x1 + 1,
       
       [high2](x0, x1) = 0,
       
       [high1](x0) = 2x0 + 1,
       
       [if_low1](x0) = 1,
       
       [if_low3](x0, x1, x2) = 0,
       
       [if_low2](x0, x1) = 2x1 + 1,
       
       [low2](x0, x1) = 0,
       
       [low1](x0) = 0,
       
       [add2](x0, x1) = 0,
       
       [add1](x0) = 4x0 + 6,
       
       [app2](x0, x1) = 2x1,
       
       [app1](x0) = 2x0 + 1,
       
       [le2](x0, x1) = 2x1,
       
       [le1](x0) = 2x0 + 2,
       
       [quot2](x0, x1) = 4x0 + 1,
       
       [quot1](x0) = 2x0 + 4,
       
       [s1](x0) = 4x0 + 1,
       
       [minus2](x0, x1) = x0,
       
       [minus1](x0) = 4x0 + 5,
       
       [filter2] = 0,
       
       [filter] = 0,
       
       [map] = 0,
       
       [quicksort] = 1,
       
       [if_high] = 0,
       
       [high] = 4,
       
       [if_low] = 0,
       
       [low] = 2,
       
       [add] = 1,
       
       [nil] = 0,
       
       [app] = 0,
       
       [false] = 0,
       
       [true] = 0,
       
       [le] = 6,
       
       [quot] = 3,
       
       [s] = 0,
       
       [0] = 0,
       
       [app'](x0, x1) = 4x0 + 4x1 + 4,
       
       [minus] = 2
      orientation:
       quot{2,#}(s1(x),s1(y)) = 4x + 1 >= x = quot{2,#}(minus2(x,y),s1(y))
       
       minus2(x,0()) = x >= x = x
       
       minus2(s1(x),s1(y)) = 4x + 1 >= x = minus2(x,y)
       
       quot2(0(),s1(y)) = 1 >= 0 = 0()
       
       quot2(s1(x),s1(y)) = 16x + 5 >= 16x + 5 = s1(quot2(minus2(x,y),s1(y)))
       
       le2(0(),y) = 2y >= 0 = true()
       
       le2(s1(x),0()) = 0 >= 0 = false()
       
       le2(s1(x),s1(y)) = 8y + 2 >= 2y = le2(x,y)
       
       app2(nil(),y) = 2y >= y = y
       
       app2(add2(n,x),y) = 2y >= 0 = add2(n,app2(x,y))
       
       low2(n,nil()) = 0 >= 0 = nil()
       
       low2(n,add2(m,x)) = 0 >= 0 = if_low3(le2(m,n),n,add2(m,x))
       
       if_low3(true(),n,add2(m,x)) = 0 >= 0 = add2(m,low2(n,x))
       
       if_low3(false(),n,add2(m,x)) = 0 >= 0 = low2(n,x)
       
       high2(n,nil()) = 0 >= 0 = nil()
       
       high2(n,add2(m,x)) = 0 >= 0 = if_high3(le2(m,n),n,add2(m,x))
       
       if_high3(true(),n,add2(m,x)) = 0 >= 0 = high2(n,x)
       
       if_high3(false(),n,add2(m,x)) = 0 >= 0 = add2(m,high2(n,x))
       
       quicksort1(nil()) = 0 >= 0 = nil()
       
       quicksort1(add2(n,x)) = 0 >= 0 = app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
       
       map2(f,nil()) = f + 6 >= 0 = nil()
       
       map2(f,add2(x,xs)) = f + 6 >= 0 = add2(app'(f,x),map2(f,xs))
       
       filter2(f,nil()) = 0 >= 0 = nil()
       
       filter2(f,add2(x,xs)) = 0 >= 0 = filter24(app'(f,x),f,x,xs)
       
       filter24(true(),f,x,xs) = 0 >= 0 = add2(x,filter2(f,xs))
       
       filter24(false(),f,x,xs) = 0 >= 0 = filter2(f,xs)
       
       app'(minus1(x8),x9) = 16x8 + 4x9 + 24 >= x8 = minus2(x8,x9)
       
       app'(minus(),x9) = 4x9 + 12 >= 4x9 + 5 = minus1(x9)
       
       app'(s(),x9) = 4x9 + 4 >= 4x9 + 1 = s1(x9)
       
       app'(quot1(x8),x9) = 8x8 + 4x9 + 20 >= 4x8 + 1 = quot2(x8,x9)
       
       app'(quot(),x9) = 4x9 + 16 >= 2x9 + 4 = quot1(x9)
       
       app'(le1(x8),x9) = 8x8 + 4x9 + 12 >= 2x9 = le2(x8,x9)
       
       app'(le(),x9) = 4x9 + 28 >= 2x9 + 2 = le1(x9)
       
       app'(app1(x8),x9) = 8x8 + 4x9 + 8 >= 2x9 = app2(x8,x9)
       
       app'(app(),x9) = 4x9 + 4 >= 2x9 + 1 = app1(x9)
       
       app'(add1(x8),x9) = 16x8 + 4x9 + 28 >= 0 = add2(x8,x9)
       
       app'(add(),x9) = 4x9 + 8 >= 4x9 + 6 = add1(x9)
       
       app'(low1(x8),x9) = 4x9 + 4 >= 0 = low2(x8,x9)
       
       app'(low(),x9) = 4x9 + 12 >= 0 = low1(x9)
       
       app'(if_low2(x8,x7),x9) = 8x7 + 4x9 + 8 >= 0 = if_low3(x8,x7,x9)
       
       app'(if_low1(x8),x9) = 4x9 + 8 >= 2x9 + 1 = if_low2(x8,x9)
       
       app'(if_low(),x9) = 4x9 + 4 >= 1 = if_low1(x9)
       
       app'(high1(x8),x9) = 8x8 + 4x9 + 8 >= 0 = high2(x8,x9)
       
       app'(high(),x9) = 4x9 + 20 >= 2x9 + 1 = high1(x9)
       
       app'(if_high2(x8,x7),x9) = 8x7 + 4x9 + 8 >= 4x9 = if_high3(x8,x7,x9)
       
       app'(if_high1(x8),x9) = 4x9 + 20 >= 2x9 + 1 = if_high2(x8,x9)
       
       app'(if_high(),x9) = 4x9 + 4 >= 4 = if_high1(x9)
       
       app'(quicksort(),x9) = 4x9 + 8 >= 0 = quicksort1(x9)
       
       app'(map1(x8),x9) = 16x8 + 4x9 + 16 >= x8 + 4x9 + 6 = map2(x8,x9)
       
       app'(map(),x9) = 4x9 + 4 >= 4x9 + 3 = map1(x9)
       
       app'(filter1(x8),x9) = 4x9 + 12 >= 0 = filter2(x8,x9)
       
       app'(filter(),x9) = 4x9 + 4 >= 2 = filter1(x9)
       
       app'(filter23(x8,x7,x6),x9) = 4x6 + 4x9 + 4 >= 0 = filter24(x8,x7,x6,x9)
       
       app'(filter22(x8,x7),x9) = 4x9 + 16 >= x9 = filter23(x8,x7,x9)
       
       app'(filter21(x8),x9) = 16x8 + 4x9 + 12 >= 3 = filter22(x8,x9)
       
       app'(filter2(),x9) = 4x9 + 4 >= 4x9 + 2 = filter21(x9)
      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:
      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