YES

Problem:
 app'(app'(minus(),x),0()) -> x
 app'(app'(minus(),app'(s(),x)),app'(s(),y)) -> app'(app'(minus(),x),y)
 app'(app'(minus(),app'(app'(minus(),x),y)),z) -> app'(app'(minus(),x),app'(app'(plus(),y),z))
 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'(plus(),0()),y) -> y
 app'(app'(plus(),app'(s(),x)),y) -> app'(s(),app'(app'(plus(),x),y))
 app'(app'(app(),nil()),k) -> k
 app'(app'(app(),l),nil()) -> l
 app'(app'(app(),app'(app'(cons(),x),l)),k) -> app'(app'(cons(),x),app'(app'(app(),l),k))
 app'(sum(),app'(app'(cons(),x),nil())) -> app'(app'(cons(),x),nil())
 app'(sum(),app'(app'(cons(),x),app'(app'(cons(),y),l))) ->
 app'(sum(),app'(app'(cons(),app'(app'(plus(),x),y)),l))
 app'(sum(),app'(app'(app(),l),app'(app'(cons(),x),app'(app'(cons(),y),k)))) ->
 app'(sum(),app'(app'(app(),l),app'(sum(),app'(app'(cons(),x),app'(app'(cons(),y),k)))))
 app'(app'(map(),f),nil()) -> nil()
 app'(app'(map(),f),app'(app'(cons(),x),xs)) -> app'(app'(cons(),app'(f,x)),app'(app'(map(),f),xs))
 app'(app'(filter(),f),nil()) -> nil()
 app'(app'(filter(),f),app'(app'(cons(),x),xs)) ->
 app'(app'(app'(app'(filter2(),app'(f,x)),f),x),xs)
 app'(app'(app'(app'(filter2(),true()),f),x),xs) -> app'(app'(cons(),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)
  minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
  quot2(0(),s1(y)) -> 0()
  quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
  plus2(0(),y) -> y
  plus2(s1(x),y) -> s1(plus2(x,y))
  app2(nil(),k) -> k
  app2(l,nil()) -> l
  app2(cons2(x,l),k) -> cons2(x,app2(l,k))
  sum1(cons2(x,nil())) -> cons2(x,nil())
  sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
  sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
  map2(f,nil()) -> nil()
  map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
  filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
  filter24(false(),f,x,xs) -> filter2(f,xs)
  app'(minus1(x9),x10) -> minus2(x9,x10)
  app'(minus(),x10) -> minus1(x10)
  app'(s(),x10) -> s1(x10)
  app'(plus1(x9),x10) -> plus2(x9,x10)
  app'(plus(),x10) -> plus1(x10)
  app'(quot1(x9),x10) -> quot2(x9,x10)
  app'(quot(),x10) -> quot1(x10)
  app'(app1(x9),x10) -> app2(x9,x10)
  app'(app(),x10) -> app1(x10)
  app'(cons1(x9),x10) -> cons2(x9,x10)
  app'(cons(),x10) -> cons1(x10)
  app'(sum(),x10) -> sum1(x10)
  app'(map1(x9),x10) -> map2(x9,x10)
  app'(map(),x10) -> map1(x10)
  app'(filter1(x9),x10) -> filter2(x9,x10)
  app'(filter(),x10) -> filter1(x10)
  app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
  app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
  app'(filter21(x9),x10) -> filter22(x9,x10)
  app'(filter2(),x10) -> filter21(x10)
  DP Processor:
   DPs:
    minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
    minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z)
    minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
    quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
    quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
    plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
    app{2,#}(cons2(x,l),k) -> app{2,#}(l,k)
    sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y)
    sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
    sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
    sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k))))
    sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
    map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
    map{2,#}(f,cons2(x,xs)) -> app'#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> app'#(f,x)
    filter{2,#}(f,cons2(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(x9),x10) -> minus{2,#}(x9,x10)
    app'#(plus1(x9),x10) -> plus{2,#}(x9,x10)
    app'#(quot1(x9),x10) -> quot{2,#}(x9,x10)
    app'#(app1(x9),x10) -> app{2,#}(x9,x10)
    app'#(sum(),x10) -> sum{1,#}(x10)
    app'#(map1(x9),x10) -> map{2,#}(x9,x10)
    app'#(filter1(x9),x10) -> filter{2,#}(x9,x10)
    app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10)
   TRS:
    minus2(x,0()) -> x
    minus2(s1(x),s1(y)) -> minus2(x,y)
    minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
    quot2(0(),s1(y)) -> 0()
    quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
    plus2(0(),y) -> y
    plus2(s1(x),y) -> s1(plus2(x,y))
    app2(nil(),k) -> k
    app2(l,nil()) -> l
    app2(cons2(x,l),k) -> cons2(x,app2(l,k))
    sum1(cons2(x,nil())) -> cons2(x,nil())
    sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
    sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
    map2(f,nil()) -> nil()
    map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
    filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
    filter24(false(),f,x,xs) -> filter2(f,xs)
    app'(minus1(x9),x10) -> minus2(x9,x10)
    app'(minus(),x10) -> minus1(x10)
    app'(s(),x10) -> s1(x10)
    app'(plus1(x9),x10) -> plus2(x9,x10)
    app'(plus(),x10) -> plus1(x10)
    app'(quot1(x9),x10) -> quot2(x9,x10)
    app'(quot(),x10) -> quot1(x10)
    app'(app1(x9),x10) -> app2(x9,x10)
    app'(app(),x10) -> app1(x10)
    app'(cons1(x9),x10) -> cons2(x9,x10)
    app'(cons(),x10) -> cons1(x10)
    app'(sum(),x10) -> sum1(x10)
    app'(map1(x9),x10) -> map2(x9,x10)
    app'(map(),x10) -> map1(x10)
    app'(filter1(x9),x10) -> filter2(x9,x10)
    app'(filter(),x10) -> filter1(x10)
    app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
    app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
    app'(filter21(x9),x10) -> filter22(x9,x10)
    app'(filter2(),x10) -> filter21(x10)
   TDG Processor:
    DPs:
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z)
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     app{2,#}(cons2(x,l),k) -> app{2,#}(l,k)
     sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y)
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k))))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     filter{2,#}(f,cons2(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(x9),x10) -> minus{2,#}(x9,x10)
     app'#(plus1(x9),x10) -> plus{2,#}(x9,x10)
     app'#(quot1(x9),x10) -> quot{2,#}(x9,x10)
     app'#(app1(x9),x10) -> app{2,#}(x9,x10)
     app'#(sum(),x10) -> sum{1,#}(x10)
     app'#(map1(x9),x10) -> map{2,#}(x9,x10)
     app'#(filter1(x9),x10) -> filter{2,#}(x9,x10)
     app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10)
    TRS:
     minus2(x,0()) -> x
     minus2(s1(x),s1(y)) -> minus2(x,y)
     minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
     quot2(0(),s1(y)) -> 0()
     quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
     plus2(0(),y) -> y
     plus2(s1(x),y) -> s1(plus2(x,y))
     app2(nil(),k) -> k
     app2(l,nil()) -> l
     app2(cons2(x,l),k) -> cons2(x,app2(l,k))
     sum1(cons2(x,nil())) -> cons2(x,nil())
     sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
     sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
     map2(f,nil()) -> nil()
     map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app'(minus1(x9),x10) -> minus2(x9,x10)
     app'(minus(),x10) -> minus1(x10)
     app'(s(),x10) -> s1(x10)
     app'(plus1(x9),x10) -> plus2(x9,x10)
     app'(plus(),x10) -> plus1(x10)
     app'(quot1(x9),x10) -> quot2(x9,x10)
     app'(quot(),x10) -> quot1(x10)
     app'(app1(x9),x10) -> app2(x9,x10)
     app'(app(),x10) -> app1(x10)
     app'(cons1(x9),x10) -> cons2(x9,x10)
     app'(cons(),x10) -> cons1(x10)
     app'(sum(),x10) -> sum1(x10)
     app'(map1(x9),x10) -> map2(x9,x10)
     app'(map(),x10) -> map1(x10)
     app'(filter1(x9),x10) -> filter2(x9,x10)
     app'(filter(),x10) -> filter1(x10)
     app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
     app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
     app'(filter21(x9),x10) -> filter22(x9,x10)
     app'(filter2(),x10) -> filter21(x10)
    graph:
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(filter1(x9),x10) -> filter{2,#}(x9,x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(map1(x9),x10) -> map{2,#}(x9,x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(sum(),x10) -> sum{1,#}(x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(app1(x9),x10) -> app{2,#}(x9,x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(quot1(x9),x10) -> quot{2,#}(x9,x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(plus1(x9),x10) -> plus{2,#}(x9,x10)
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(minus1(x9),x10) -> minus{2,#}(x9,x10)
     app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     app'#(filter1(x9),x10) -> filter{2,#}(x9,x10) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
     app'#(filter1(x9),x10) -> filter{2,#}(x9,x10) ->
     filter{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     app'#(map1(x9),x10) -> map{2,#}(x9,x10) ->
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     app'#(map1(x9),x10) -> map{2,#}(x9,x10) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     app'#(app1(x9),x10) -> app{2,#}(x9,x10) ->
     app{2,#}(cons2(x,l),k) -> app{2,#}(l,k)
     app'#(quot1(x9),x10) -> quot{2,#}(x9,x10) ->
     quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
     app'#(quot1(x9),x10) -> quot{2,#}(x9,x10) ->
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     app'#(plus1(x9),x10) -> plus{2,#}(x9,x10) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     app'#(minus1(x9),x10) -> minus{2,#}(x9,x10) ->
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
     app'#(minus1(x9),x10) -> minus{2,#}(x9,x10) ->
     minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z)
     app'#(minus1(x9),x10) -> minus{2,#}(x9,x10) ->
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     app'#(sum(),x10) -> sum{1,#}(x10) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
     app'#(sum(),x10) -> sum{1,#}(x10) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k))))
     app'#(sum(),x10) -> sum{1,#}(x10) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
     app'#(sum(),x10) -> sum{1,#}(x10) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
     app'#(sum(),x10) -> sum{1,#}(x10) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(filter1(x9),x10) -> filter{2,#}(x9,x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(map1(x9),x10) -> map{2,#}(x9,x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(sum(),x10) -> sum{1,#}(x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(app1(x9),x10) -> app{2,#}(x9,x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(quot1(x9),x10) -> quot{2,#}(x9,x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(plus1(x9),x10) -> plus{2,#}(x9,x10)
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x) ->
     app'#(minus1(x9),x10) -> minus{2,#}(x9,x10)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> app'#(f,x)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l)) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l)) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k))))
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l)) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l)) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l)) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y)
     sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k))) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k))) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k))))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k))) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k))) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k))) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y)
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k))))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
     sum{1,#}(cons2(x,cons2(y,l))) -> plus{2,#}(x,y)
     sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> app{2,#}(l,sum1(cons2(x,cons2(y,k)))) ->
     app{2,#}(cons2(x,l),k) -> app{2,#}(l,k)
     app{2,#}(cons2(x,l),k) -> app{2,#}(l,k) ->
     app{2,#}(cons2(x,l),k) -> app{2,#}(l,k)
     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,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
     minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z)
     quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
     minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z)
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z)) ->
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z)) ->
     minus{2,#}(minus2(x,y),z) -> plus{2,#}(y,z)
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z)) ->
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
    SCC Processor:
     #sccs: 6
     #rules: 17
     #arcs: 73/676
     DPs:
      filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> app'#(f,x)
      app'#(map1(x9),x10) -> map{2,#}(x9,x10)
      map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
      map{2,#}(f,cons2(x,xs)) -> app'#(f,x)
      app'#(filter1(x9),x10) -> filter{2,#}(x9,x10)
      filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs)
      filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
      app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      app2(nil(),k) -> k
      app2(l,nil()) -> l
      app2(cons2(x,l),k) -> cons2(x,app2(l,k))
      sum1(cons2(x,nil())) -> cons2(x,nil())
      sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
      sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x9),x10) -> minus2(x9,x10)
      app'(minus(),x10) -> minus1(x10)
      app'(s(),x10) -> s1(x10)
      app'(plus1(x9),x10) -> plus2(x9,x10)
      app'(plus(),x10) -> plus1(x10)
      app'(quot1(x9),x10) -> quot2(x9,x10)
      app'(quot(),x10) -> quot1(x10)
      app'(app1(x9),x10) -> app2(x9,x10)
      app'(app(),x10) -> app1(x10)
      app'(cons1(x9),x10) -> cons2(x9,x10)
      app'(cons(),x10) -> cons1(x10)
      app'(sum(),x10) -> sum1(x10)
      app'(map1(x9),x10) -> map2(x9,x10)
      app'(map(),x10) -> map1(x10)
      app'(filter1(x9),x10) -> filter2(x9,x10)
      app'(filter(),x10) -> filter1(x10)
      app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
      app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
      app'(filter21(x9),x10) -> filter22(x9,x10)
      app'(filter2(),x10) -> filter21(x10)
     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(x9),x10) -> map{2,#}(x9,x10)
        app'#(filter1(x9),x10) -> filter{2,#}(x9,x10)
        filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
        app'#(filter23(x9,x8,x7),x10) -> filter2{4,#}(x9,x8,x7,x10)
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        app2(nil(),k) -> k
        app2(l,nil()) -> l
        app2(cons2(x,l),k) -> cons2(x,app2(l,k))
        sum1(cons2(x,nil())) -> cons2(x,nil())
        sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
        sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x9),x10) -> minus2(x9,x10)
        app'(minus(),x10) -> minus1(x10)
        app'(s(),x10) -> s1(x10)
        app'(plus1(x9),x10) -> plus2(x9,x10)
        app'(plus(),x10) -> plus1(x10)
        app'(quot1(x9),x10) -> quot2(x9,x10)
        app'(quot(),x10) -> quot1(x10)
        app'(app1(x9),x10) -> app2(x9,x10)
        app'(app(),x10) -> app1(x10)
        app'(cons1(x9),x10) -> cons2(x9,x10)
        app'(cons(),x10) -> cons1(x10)
        app'(sum(),x10) -> sum1(x10)
        app'(map1(x9),x10) -> map2(x9,x10)
        app'(map(),x10) -> map1(x10)
        app'(filter1(x9),x10) -> filter2(x9,x10)
        app'(filter(),x10) -> filter1(x10)
        app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
        app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
        app'(filter21(x9),x10) -> filter22(x9,x10)
        app'(filter2(),x10) -> filter21(x10)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 20/25
       
     
     DPs:
      sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
      sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
      sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      app2(nil(),k) -> k
      app2(l,nil()) -> l
      app2(cons2(x,l),k) -> cons2(x,app2(l,k))
      sum1(cons2(x,nil())) -> cons2(x,nil())
      sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
      sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x9),x10) -> minus2(x9,x10)
      app'(minus(),x10) -> minus1(x10)
      app'(s(),x10) -> s1(x10)
      app'(plus1(x9),x10) -> plus2(x9,x10)
      app'(plus(),x10) -> plus1(x10)
      app'(quot1(x9),x10) -> quot2(x9,x10)
      app'(quot(),x10) -> quot1(x10)
      app'(app1(x9),x10) -> app2(x9,x10)
      app'(app(),x10) -> app1(x10)
      app'(cons1(x9),x10) -> cons2(x9,x10)
      app'(cons(),x10) -> cons1(x10)
      app'(sum(),x10) -> sum1(x10)
      app'(map1(x9),x10) -> map2(x9,x10)
      app'(map(),x10) -> map1(x10)
      app'(filter1(x9),x10) -> filter2(x9,x10)
      app'(filter(),x10) -> filter1(x10)
      app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
      app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
      app'(filter21(x9),x10) -> filter22(x9,x10)
      app'(filter2(),x10) -> filter21(x10)
     EDG Processor:
      DPs:
       sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
      TRS:
       minus2(x,0()) -> x
       minus2(s1(x),s1(y)) -> minus2(x,y)
       minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
       quot2(0(),s1(y)) -> 0()
       quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
       plus2(0(),y) -> y
       plus2(s1(x),y) -> s1(plus2(x,y))
       app2(nil(),k) -> k
       app2(l,nil()) -> l
       app2(cons2(x,l),k) -> cons2(x,app2(l,k))
       sum1(cons2(x,nil())) -> cons2(x,nil())
       sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
       sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
       map2(f,nil()) -> nil()
       map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
       filter2(f,nil()) -> nil()
       filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
       filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
       filter24(false(),f,x,xs) -> filter2(f,xs)
       app'(minus1(x9),x10) -> minus2(x9,x10)
       app'(minus(),x10) -> minus1(x10)
       app'(s(),x10) -> s1(x10)
       app'(plus1(x9),x10) -> plus2(x9,x10)
       app'(plus(),x10) -> plus1(x10)
       app'(quot1(x9),x10) -> quot2(x9,x10)
       app'(quot(),x10) -> quot1(x10)
       app'(app1(x9),x10) -> app2(x9,x10)
       app'(app(),x10) -> app1(x10)
       app'(cons1(x9),x10) -> cons2(x9,x10)
       app'(cons(),x10) -> cons1(x10)
       app'(sum(),x10) -> sum1(x10)
       app'(map1(x9),x10) -> map2(x9,x10)
       app'(map(),x10) -> map1(x10)
       app'(filter1(x9),x10) -> filter2(x9,x10)
       app'(filter(),x10) -> filter1(x10)
       app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
       app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
       app'(filter21(x9),x10) -> filter22(x9,x10)
       app'(filter2(),x10) -> filter21(x10)
      graph:
       sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l)) ->
       sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k))) ->
       sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
       sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(cons2(x,cons2(y,k)))
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k))))) ->
       sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
      SCC Processor:
       #sccs: 2
       #rules: 2
       #arcs: 5/9
       DPs:
        sum{1,#}(app2(l,cons2(x,cons2(y,k)))) -> sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        app2(nil(),k) -> k
        app2(l,nil()) -> l
        app2(cons2(x,l),k) -> cons2(x,app2(l,k))
        sum1(cons2(x,nil())) -> cons2(x,nil())
        sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
        sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x9),x10) -> minus2(x9,x10)
        app'(minus(),x10) -> minus1(x10)
        app'(s(),x10) -> s1(x10)
        app'(plus1(x9),x10) -> plus2(x9,x10)
        app'(plus(),x10) -> plus1(x10)
        app'(quot1(x9),x10) -> quot2(x9,x10)
        app'(quot(),x10) -> quot1(x10)
        app'(app1(x9),x10) -> app2(x9,x10)
        app'(app(),x10) -> app1(x10)
        app'(cons1(x9),x10) -> cons2(x9,x10)
        app'(cons(),x10) -> cons1(x10)
        app'(sum(),x10) -> sum1(x10)
        app'(map1(x9),x10) -> map2(x9,x10)
        app'(map(),x10) -> map1(x10)
        app'(filter1(x9),x10) -> filter2(x9,x10)
        app'(filter(),x10) -> filter1(x10)
        app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
        app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
        app'(filter21(x9),x10) -> filter22(x9,x10)
        app'(filter2(),x10) -> filter21(x10)
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [sum{1,#}](x0) = 2x0 + 1,
         
         [filter21](x0) = 1,
         
         [filter22](x0, x1) = x1 + 2,
         
         [filter24](x0, x1, x2, x3) = x3 + 4,
         
         [filter23](x0, x1, x2) = 4x1 + x2 + 1,
         
         [filter2](x0, x1) = x1 + 2,
         
         [filter1](x0) = 4,
         
         [map2](x0, x1) = x1 + 2,
         
         [map1](x0) = 1,
         
         [sum1](x0) = 2,
         
         [cons2](x0, x1) = x1 + 2,
         
         [cons1](x0) = 3,
         
         [app2](x0, x1) = 4x0 + x1 + 2,
         
         [app1](x0) = x0 + 3,
         
         [quot2](x0, x1) = x1 + 1,
         
         [quot1](x0) = 1,
         
         [plus2](x0, x1) = x1 + 2,
         
         [plus1](x0) = 4,
         
         [s1](x0) = x0,
         
         [minus2](x0, x1) = 2x0,
         
         [minus1](x0) = x0,
         
         [false] = 0,
         
         [true] = 0,
         
         [filter2] = 6,
         
         [filter] = 1,
         
         [map] = 1,
         
         [sum] = 1,
         
         [cons] = 1,
         
         [nil] = 0,
         
         [app] = 1,
         
         [quot] = 4,
         
         [plus] = 5,
         
         [s] = 4,
         
         [0] = 1,
         
         [app'](x0, x1) = 4x0 + x1,
         
         [minus] = 0
        orientation:
         sum{1,#}(app2(l,cons2(x,cons2(y,k)))) = 2k + 8l + 13 >= 8l + 9 = sum{1,#}(app2(l,sum1(cons2(x,cons2(y,k)))))
         
         minus2(x,0()) = 2x >= x = x
         
         minus2(s1(x),s1(y)) = 2x >= 2x = minus2(x,y)
         
         minus2(minus2(x,y),z) = 4x >= 2x = minus2(x,plus2(y,z))
         
         quot2(0(),s1(y)) = y + 1 >= 1 = 0()
         
         quot2(s1(x),s1(y)) = y + 1 >= y + 1 = s1(quot2(minus2(x,y),s1(y)))
         
         plus2(0(),y) = y + 2 >= y = y
         
         plus2(s1(x),y) = y + 2 >= y + 2 = s1(plus2(x,y))
         
         app2(nil(),k) = k + 2 >= k = k
         
         app2(l,nil()) = 4l + 2 >= l = l
         
         app2(cons2(x,l),k) = k + 4l + 10 >= k + 4l + 4 = cons2(x,app2(l,k))
         
         sum1(cons2(x,nil())) = 2 >= 2 = cons2(x,nil())
         
         sum1(cons2(x,cons2(y,l))) = 2 >= 2 = sum1(cons2(plus2(x,y),l))
         
         sum1(app2(l,cons2(x,cons2(y,k)))) = 2 >= 2 = sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
         
         map2(f,nil()) = 2 >= 0 = nil()
         
         map2(f,cons2(x,xs)) = xs + 4 >= xs + 4 = cons2(app'(f,x),map2(f,xs))
         
         filter2(f,nil()) = 2 >= 0 = nil()
         
         filter2(f,cons2(x,xs)) = xs + 4 >= xs + 4 = filter24(app'(f,x),f,x,xs)
         
         filter24(true(),f,x,xs) = xs + 4 >= xs + 4 = cons2(x,filter2(f,xs))
         
         filter24(false(),f,x,xs) = xs + 4 >= xs + 2 = filter2(f,xs)
         
         app'(minus1(x9),x10) = x10 + 4x9 >= 2x9 = minus2(x9,x10)
         
         app'(minus(),x10) = x10 >= x10 = minus1(x10)
         
         app'(s(),x10) = x10 + 16 >= x10 = s1(x10)
         
         app'(plus1(x9),x10) = x10 + 16 >= x10 + 2 = plus2(x9,x10)
         
         app'(plus(),x10) = x10 + 20 >= 4 = plus1(x10)
         
         app'(quot1(x9),x10) = x10 + 4 >= x10 + 1 = quot2(x9,x10)
         
         app'(quot(),x10) = x10 + 16 >= 1 = quot1(x10)
         
         app'(app1(x9),x10) = x10 + 4x9 + 12 >= x10 + 4x9 + 2 = app2(x9,x10)
         
         app'(app(),x10) = x10 + 4 >= x10 + 3 = app1(x10)
         
         app'(cons1(x9),x10) = x10 + 12 >= x10 + 2 = cons2(x9,x10)
         
         app'(cons(),x10) = x10 + 4 >= 3 = cons1(x10)
         
         app'(sum(),x10) = x10 + 4 >= 2 = sum1(x10)
         
         app'(map1(x9),x10) = x10 + 4 >= x10 + 2 = map2(x9,x10)
         
         app'(map(),x10) = x10 + 4 >= 1 = map1(x10)
         
         app'(filter1(x9),x10) = x10 + 16 >= x10 + 2 = filter2(x9,x10)
         
         app'(filter(),x10) = x10 + 4 >= 4 = filter1(x10)
         
         app'(filter23(x9,x8,x7),x10) = x10 + 4x7 + 16x8 + 4 >= x10 + 4 = filter24(x9,x8,x7,x10)
         
         app'(filter22(x9,x8),x10) = x10 + 4x8 + 8 >= x10 + 4x8 + 1 = filter23(x9,x8,x10)
         
         app'(filter21(x9),x10) = x10 + 4 >= x10 + 2 = filter22(x9,x10)
         
         app'(filter2(),x10) = x10 + 24 >= 1 = filter21(x10)
        problem:
         DPs:
          
         TRS:
          minus2(x,0()) -> x
          minus2(s1(x),s1(y)) -> minus2(x,y)
          minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
          quot2(0(),s1(y)) -> 0()
          quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
          plus2(0(),y) -> y
          plus2(s1(x),y) -> s1(plus2(x,y))
          app2(nil(),k) -> k
          app2(l,nil()) -> l
          app2(cons2(x,l),k) -> cons2(x,app2(l,k))
          sum1(cons2(x,nil())) -> cons2(x,nil())
          sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
          sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
          map2(f,nil()) -> nil()
          map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
          filter2(f,nil()) -> nil()
          filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
          filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
          filter24(false(),f,x,xs) -> filter2(f,xs)
          app'(minus1(x9),x10) -> minus2(x9,x10)
          app'(minus(),x10) -> minus1(x10)
          app'(s(),x10) -> s1(x10)
          app'(plus1(x9),x10) -> plus2(x9,x10)
          app'(plus(),x10) -> plus1(x10)
          app'(quot1(x9),x10) -> quot2(x9,x10)
          app'(quot(),x10) -> quot1(x10)
          app'(app1(x9),x10) -> app2(x9,x10)
          app'(app(),x10) -> app1(x10)
          app'(cons1(x9),x10) -> cons2(x9,x10)
          app'(cons(),x10) -> cons1(x10)
          app'(sum(),x10) -> sum1(x10)
          app'(map1(x9),x10) -> map2(x9,x10)
          app'(map(),x10) -> map1(x10)
          app'(filter1(x9),x10) -> filter2(x9,x10)
          app'(filter(),x10) -> filter1(x10)
          app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
          app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
          app'(filter21(x9),x10) -> filter22(x9,x10)
          app'(filter2(),x10) -> filter21(x10)
        Qed
       
       DPs:
        sum{1,#}(cons2(x,cons2(y,l))) -> sum{1,#}(cons2(plus2(x,y),l))
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        app2(nil(),k) -> k
        app2(l,nil()) -> l
        app2(cons2(x,l),k) -> cons2(x,app2(l,k))
        sum1(cons2(x,nil())) -> cons2(x,nil())
        sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
        sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x9),x10) -> minus2(x9,x10)
        app'(minus(),x10) -> minus1(x10)
        app'(s(),x10) -> s1(x10)
        app'(plus1(x9),x10) -> plus2(x9,x10)
        app'(plus(),x10) -> plus1(x10)
        app'(quot1(x9),x10) -> quot2(x9,x10)
        app'(quot(),x10) -> quot1(x10)
        app'(app1(x9),x10) -> app2(x9,x10)
        app'(app(),x10) -> app1(x10)
        app'(cons1(x9),x10) -> cons2(x9,x10)
        app'(cons(),x10) -> cons1(x10)
        app'(sum(),x10) -> sum1(x10)
        app'(map1(x9),x10) -> map2(x9,x10)
        app'(map(),x10) -> map1(x10)
        app'(filter1(x9),x10) -> filter2(x9,x10)
        app'(filter(),x10) -> filter1(x10)
        app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
        app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
        app'(filter21(x9),x10) -> filter22(x9,x10)
        app'(filter2(),x10) -> filter21(x10)
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [sum{1,#}](x0) = 2x0,
         
         [filter21](x0) = 1,
         
         [filter22](x0, x1) = 3/2x1 + 1,
         
         [filter24](x0, x1, x2, x3) = x3 + 1,
         
         [filter23](x0, x1, x2) = 3x1 + 1/2,
         
         [filter2](x0, x1) = x1,
         
         [filter1](x0) = 2x0,
         
         [map2](x0, x1) = x0 + x1 + 2,
         
         [map1](x0) = 2x0 + 1,
         
         [sum1](x0) = 2,
         
         [cons2](x0, x1) = x1 + 1,
         
         [cons1](x0) = 1,
         
         [app2](x0, x1) = 2x0 + 2x1 + 2,
         
         [app1](x0) = x0 + 2,
         
         [quot2](x0, x1) = 1,
         
         [quot1](x0) = 1,
         
         [plus2](x0, x1) = 1/2x0 + x1,
         
         [plus1](x0) = x0,
         
         [s1](x0) = x0,
         
         [minus2](x0, x1) = 2x0,
         
         [minus1](x0) = x0,
         
         [false] = 0,
         
         [true] = 0,
         
         [filter2] = 3,
         
         [filter] = 2,
         
         [map] = 2,
         
         [sum] = 2,
         
         [cons] = 3/2,
         
         [nil] = 0,
         
         [app] = 2,
         
         [quot] = 3/2,
         
         [plus] = 1,
         
         [s] = 1/2,
         
         [0] = 0,
         
         [app'](x0, x1) = 2x0 + 2x1,
         
         [minus] = 5/2
        orientation:
         sum{1,#}(cons2(x,cons2(y,l))) = 2l + 4 >= 2l + 2 = sum{1,#}(cons2(plus2(x,y),l))
         
         minus2(x,0()) = 2x >= x = x
         
         minus2(s1(x),s1(y)) = 2x >= 2x = minus2(x,y)
         
         minus2(minus2(x,y),z) = 4x >= 2x = minus2(x,plus2(y,z))
         
         quot2(0(),s1(y)) = 1 >= 0 = 0()
         
         quot2(s1(x),s1(y)) = 1 >= 1 = s1(quot2(minus2(x,y),s1(y)))
         
         plus2(0(),y) = y >= y = y
         
         plus2(s1(x),y) = 1/2x + y >= 1/2x + y = s1(plus2(x,y))
         
         app2(nil(),k) = 2k + 2 >= k = k
         
         app2(l,nil()) = 2l + 2 >= l = l
         
         app2(cons2(x,l),k) = 2k + 2l + 4 >= 2k + 2l + 3 = cons2(x,app2(l,k))
         
         sum1(cons2(x,nil())) = 2 >= 1 = cons2(x,nil())
         
         sum1(cons2(x,cons2(y,l))) = 2 >= 2 = sum1(cons2(plus2(x,y),l))
         
         sum1(app2(l,cons2(x,cons2(y,k)))) = 2 >= 2 = sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
         
         map2(f,nil()) = f + 2 >= 0 = nil()
         
         map2(f,cons2(x,xs)) = f + xs + 3 >= f + xs + 3 = cons2(app'(f,x),map2(f,xs))
         
         filter2(f,nil()) = 0 >= 0 = nil()
         
         filter2(f,cons2(x,xs)) = xs + 1 >= xs + 1 = filter24(app'(f,x),f,x,xs)
         
         filter24(true(),f,x,xs) = xs + 1 >= xs + 1 = cons2(x,filter2(f,xs))
         
         filter24(false(),f,x,xs) = xs + 1 >= xs = filter2(f,xs)
         
         app'(minus1(x9),x10) = 2x10 + 2x9 >= 2x9 = minus2(x9,x10)
         
         app'(minus(),x10) = 2x10 + 5 >= x10 = minus1(x10)
         
         app'(s(),x10) = 2x10 + 1 >= x10 = s1(x10)
         
         app'(plus1(x9),x10) = 2x10 + 2x9 >= x10 + 1/2x9 = plus2(x9,x10)
         
         app'(plus(),x10) = 2x10 + 2 >= x10 = plus1(x10)
         
         app'(quot1(x9),x10) = 2x10 + 2 >= 1 = quot2(x9,x10)
         
         app'(quot(),x10) = 2x10 + 3 >= 1 = quot1(x10)
         
         app'(app1(x9),x10) = 2x10 + 2x9 + 4 >= 2x10 + 2x9 + 2 = app2(x9,x10)
         
         app'(app(),x10) = 2x10 + 4 >= x10 + 2 = app1(x10)
         
         app'(cons1(x9),x10) = 2x10 + 2 >= x10 + 1 = cons2(x9,x10)
         
         app'(cons(),x10) = 2x10 + 3 >= 1 = cons1(x10)
         
         app'(sum(),x10) = 2x10 + 4 >= 2 = sum1(x10)
         
         app'(map1(x9),x10) = 2x10 + 4x9 + 2 >= x10 + x9 + 2 = map2(x9,x10)
         
         app'(map(),x10) = 2x10 + 4 >= 2x10 + 1 = map1(x10)
         
         app'(filter1(x9),x10) = 2x10 + 4x9 >= x10 = filter2(x9,x10)
         
         app'(filter(),x10) = 2x10 + 4 >= 2x10 = filter1(x10)
         
         app'(filter23(x9,x8,x7),x10) = 2x10 + 6x8 + 1 >= x10 + 1 = filter24(x9,x8,x7,x10)
         
         app'(filter22(x9,x8),x10) = 2x10 + 3x8 + 2 >= 3x8 + 1/2 = filter23(x9,x8,x10)
         
         app'(filter21(x9),x10) = 2x10 + 2 >= 3/2x10 + 1 = filter22(x9,x10)
         
         app'(filter2(),x10) = 2x10 + 6 >= 1 = filter21(x10)
        problem:
         DPs:
          
         TRS:
          minus2(x,0()) -> x
          minus2(s1(x),s1(y)) -> minus2(x,y)
          minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
          quot2(0(),s1(y)) -> 0()
          quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
          plus2(0(),y) -> y
          plus2(s1(x),y) -> s1(plus2(x,y))
          app2(nil(),k) -> k
          app2(l,nil()) -> l
          app2(cons2(x,l),k) -> cons2(x,app2(l,k))
          sum1(cons2(x,nil())) -> cons2(x,nil())
          sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
          sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
          map2(f,nil()) -> nil()
          map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
          filter2(f,nil()) -> nil()
          filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
          filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
          filter24(false(),f,x,xs) -> filter2(f,xs)
          app'(minus1(x9),x10) -> minus2(x9,x10)
          app'(minus(),x10) -> minus1(x10)
          app'(s(),x10) -> s1(x10)
          app'(plus1(x9),x10) -> plus2(x9,x10)
          app'(plus(),x10) -> plus1(x10)
          app'(quot1(x9),x10) -> quot2(x9,x10)
          app'(quot(),x10) -> quot1(x10)
          app'(app1(x9),x10) -> app2(x9,x10)
          app'(app(),x10) -> app1(x10)
          app'(cons1(x9),x10) -> cons2(x9,x10)
          app'(cons(),x10) -> cons1(x10)
          app'(sum(),x10) -> sum1(x10)
          app'(map1(x9),x10) -> map2(x9,x10)
          app'(map(),x10) -> map1(x10)
          app'(filter1(x9),x10) -> filter2(x9,x10)
          app'(filter(),x10) -> filter1(x10)
          app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
          app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
          app'(filter21(x9),x10) -> filter22(x9,x10)
          app'(filter2(),x10) -> filter21(x10)
        Qed
     
     DPs:
      app{2,#}(cons2(x,l),k) -> app{2,#}(l,k)
     TRS:
      minus2(x,0()) -> x
      minus2(s1(x),s1(y)) -> minus2(x,y)
      minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      app2(nil(),k) -> k
      app2(l,nil()) -> l
      app2(cons2(x,l),k) -> cons2(x,app2(l,k))
      sum1(cons2(x,nil())) -> cons2(x,nil())
      sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
      sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x9),x10) -> minus2(x9,x10)
      app'(minus(),x10) -> minus1(x10)
      app'(s(),x10) -> s1(x10)
      app'(plus1(x9),x10) -> plus2(x9,x10)
      app'(plus(),x10) -> plus1(x10)
      app'(quot1(x9),x10) -> quot2(x9,x10)
      app'(quot(),x10) -> quot1(x10)
      app'(app1(x9),x10) -> app2(x9,x10)
      app'(app(),x10) -> app1(x10)
      app'(cons1(x9),x10) -> cons2(x9,x10)
      app'(cons(),x10) -> cons1(x10)
      app'(sum(),x10) -> sum1(x10)
      app'(map1(x9),x10) -> map2(x9,x10)
      app'(map(),x10) -> map1(x10)
      app'(filter1(x9),x10) -> filter2(x9,x10)
      app'(filter(),x10) -> filter1(x10)
      app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
      app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
      app'(filter21(x9),x10) -> filter22(x9,x10)
      app'(filter2(),x10) -> filter21(x10)
     Subterm Criterion Processor:
      simple projection:
       pi(app{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        app2(nil(),k) -> k
        app2(l,nil()) -> l
        app2(cons2(x,l),k) -> cons2(x,app2(l,k))
        sum1(cons2(x,nil())) -> cons2(x,nil())
        sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
        sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x9),x10) -> minus2(x9,x10)
        app'(minus(),x10) -> minus1(x10)
        app'(s(),x10) -> s1(x10)
        app'(plus1(x9),x10) -> plus2(x9,x10)
        app'(plus(),x10) -> plus1(x10)
        app'(quot1(x9),x10) -> quot2(x9,x10)
        app'(quot(),x10) -> quot1(x10)
        app'(app1(x9),x10) -> app2(x9,x10)
        app'(app(),x10) -> app1(x10)
        app'(cons1(x9),x10) -> cons2(x9,x10)
        app'(cons(),x10) -> cons1(x10)
        app'(sum(),x10) -> sum1(x10)
        app'(map1(x9),x10) -> map2(x9,x10)
        app'(map(),x10) -> map1(x10)
        app'(filter1(x9),x10) -> filter2(x9,x10)
        app'(filter(),x10) -> filter1(x10)
        app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
        app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
        app'(filter21(x9),x10) -> filter22(x9,x10)
        app'(filter2(),x10) -> filter21(x10)
      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)
      minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
      quot2(0(),s1(y)) -> 0()
      quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      app2(nil(),k) -> k
      app2(l,nil()) -> l
      app2(cons2(x,l),k) -> cons2(x,app2(l,k))
      sum1(cons2(x,nil())) -> cons2(x,nil())
      sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
      sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app'(minus1(x9),x10) -> minus2(x9,x10)
      app'(minus(),x10) -> minus1(x10)
      app'(s(),x10) -> s1(x10)
      app'(plus1(x9),x10) -> plus2(x9,x10)
      app'(plus(),x10) -> plus1(x10)
      app'(quot1(x9),x10) -> quot2(x9,x10)
      app'(quot(),x10) -> quot1(x10)
      app'(app1(x9),x10) -> app2(x9,x10)
      app'(app(),x10) -> app1(x10)
      app'(cons1(x9),x10) -> cons2(x9,x10)
      app'(cons(),x10) -> cons1(x10)
      app'(sum(),x10) -> sum1(x10)
      app'(map1(x9),x10) -> map2(x9,x10)
      app'(map(),x10) -> map1(x10)
      app'(filter1(x9),x10) -> filter2(x9,x10)
      app'(filter(),x10) -> filter1(x10)
      app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
      app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
      app'(filter21(x9),x10) -> filter22(x9,x10)
      app'(filter2(),x10) -> filter21(x10)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [quot{2,#}](x0, x1) = 4x0 + 2x1 + 1,
       
       [filter21](x0) = 4x0 + 4,
       
       [filter22](x0, x1) = 4x0 + 3x1,
       
       [filter24](x0, x1, x2, x3) = 5,
       
       [filter23](x0, x1, x2) = x2 + 2,
       
       [filter2](x0, x1) = 5,
       
       [filter1](x0) = 4x0 + 1,
       
       [map2](x0, x1) = x0 + 4,
       
       [map1](x0) = 2x0 + 1,
       
       [sum1](x0) = 1,
       
       [cons2](x0, x1) = 1,
       
       [cons1](x0) = 4x0,
       
       [app2](x0, x1) = 4x0 + 2x1 + 4,
       
       [app1](x0) = 4x0 + 4,
       
       [quot2](x0, x1) = 2x0 + x1 + 4,
       
       [quot1](x0) = 2x0 + 1,
       
       [plus2](x0, x1) = 2x0 + 2x1 + 7,
       
       [plus1](x0) = 4x0 + 4,
       
       [s1](x0) = x0 + 2,
       
       [minus2](x0, x1) = x0 + 1,
       
       [minus1](x0) = x0,
       
       [false] = 0,
       
       [true] = 0,
       
       [filter2] = 4,
       
       [filter] = 0,
       
       [map] = 2,
       
       [sum] = 0,
       
       [cons] = 3,
       
       [nil] = 0,
       
       [app] = 1,
       
       [quot] = 0,
       
       [plus] = 4,
       
       [s] = 3,
       
       [0] = 4,
       
       [app'](x0, x1) = x0 + 4x1 + 4,
       
       [minus] = 1
      orientation:
       quot{2,#}(s1(x),s1(y)) = 4x + 2y + 13 >= 4x + 2y + 9 = quot{2,#}(minus2(x,y),s1(y))
       
       minus2(x,0()) = x + 1 >= x = x
       
       minus2(s1(x),s1(y)) = x + 3 >= x + 1 = minus2(x,y)
       
       minus2(minus2(x,y),z) = x + 2 >= x + 1 = minus2(x,plus2(y,z))
       
       quot2(0(),s1(y)) = y + 14 >= 4 = 0()
       
       quot2(s1(x),s1(y)) = 2x + y + 10 >= 2x + y + 10 = s1(quot2(minus2(x,y),s1(y)))
       
       plus2(0(),y) = 2y + 15 >= y = y
       
       plus2(s1(x),y) = 2x + 2y + 11 >= 2x + 2y + 9 = s1(plus2(x,y))
       
       app2(nil(),k) = 2k + 4 >= k = k
       
       app2(l,nil()) = 4l + 4 >= l = l
       
       app2(cons2(x,l),k) = 2k + 8 >= 1 = cons2(x,app2(l,k))
       
       sum1(cons2(x,nil())) = 1 >= 1 = cons2(x,nil())
       
       sum1(cons2(x,cons2(y,l))) = 1 >= 1 = sum1(cons2(plus2(x,y),l))
       
       sum1(app2(l,cons2(x,cons2(y,k)))) = 1 >= 1 = sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
       
       map2(f,nil()) = f + 4 >= 0 = nil()
       
       map2(f,cons2(x,xs)) = f + 4 >= 1 = cons2(app'(f,x),map2(f,xs))
       
       filter2(f,nil()) = 5 >= 0 = nil()
       
       filter2(f,cons2(x,xs)) = 5 >= 5 = filter24(app'(f,x),f,x,xs)
       
       filter24(true(),f,x,xs) = 5 >= 1 = cons2(x,filter2(f,xs))
       
       filter24(false(),f,x,xs) = 5 >= 5 = filter2(f,xs)
       
       app'(minus1(x9),x10) = 4x10 + x9 + 4 >= x9 + 1 = minus2(x9,x10)
       
       app'(minus(),x10) = 4x10 + 5 >= x10 = minus1(x10)
       
       app'(s(),x10) = 4x10 + 7 >= x10 + 2 = s1(x10)
       
       app'(plus1(x9),x10) = 4x10 + 4x9 + 8 >= 2x10 + 2x9 + 7 = plus2(x9,x10)
       
       app'(plus(),x10) = 4x10 + 8 >= 4x10 + 4 = plus1(x10)
       
       app'(quot1(x9),x10) = 4x10 + 2x9 + 5 >= x10 + 2x9 + 4 = quot2(x9,x10)
       
       app'(quot(),x10) = 4x10 + 4 >= 2x10 + 1 = quot1(x10)
       
       app'(app1(x9),x10) = 4x10 + 4x9 + 8 >= 2x10 + 4x9 + 4 = app2(x9,x10)
       
       app'(app(),x10) = 4x10 + 5 >= 4x10 + 4 = app1(x10)
       
       app'(cons1(x9),x10) = 4x10 + 4x9 + 4 >= 1 = cons2(x9,x10)
       
       app'(cons(),x10) = 4x10 + 7 >= 4x10 = cons1(x10)
       
       app'(sum(),x10) = 4x10 + 4 >= 1 = sum1(x10)
       
       app'(map1(x9),x10) = 4x10 + 2x9 + 5 >= x9 + 4 = map2(x9,x10)
       
       app'(map(),x10) = 4x10 + 6 >= 2x10 + 1 = map1(x10)
       
       app'(filter1(x9),x10) = 4x10 + 4x9 + 5 >= 5 = filter2(x9,x10)
       
       app'(filter(),x10) = 4x10 + 4 >= 4x10 + 1 = filter1(x10)
       
       app'(filter23(x9,x8,x7),x10) = 4x10 + x7 + 6 >= 5 = filter24(x9,x8,x7,x10)
       
       app'(filter22(x9,x8),x10) = 4x10 + 3x8 + 4x9 + 4 >= x10 + 2 = filter23(x9,x8,x10)
       
       app'(filter21(x9),x10) = 4x10 + 4x9 + 8 >= 3x10 + 4x9 = filter22(x9,x10)
       
       app'(filter2(),x10) = 4x10 + 8 >= 4x10 + 4 = filter21(x10)
      problem:
       DPs:
        
       TRS:
        minus2(x,0()) -> x
        minus2(s1(x),s1(y)) -> minus2(x,y)
        minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
        quot2(0(),s1(y)) -> 0()
        quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        app2(nil(),k) -> k
        app2(l,nil()) -> l
        app2(cons2(x,l),k) -> cons2(x,app2(l,k))
        sum1(cons2(x,nil())) -> cons2(x,nil())
        sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
        sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app'(minus1(x9),x10) -> minus2(x9,x10)
        app'(minus(),x10) -> minus1(x10)
        app'(s(),x10) -> s1(x10)
        app'(plus1(x9),x10) -> plus2(x9,x10)
        app'(plus(),x10) -> plus1(x10)
        app'(quot1(x9),x10) -> quot2(x9,x10)
        app'(quot(),x10) -> quot1(x10)
        app'(app1(x9),x10) -> app2(x9,x10)
        app'(app(),x10) -> app1(x10)
        app'(cons1(x9),x10) -> cons2(x9,x10)
        app'(cons(),x10) -> cons1(x10)
        app'(sum(),x10) -> sum1(x10)
        app'(map1(x9),x10) -> map2(x9,x10)
        app'(map(),x10) -> map1(x10)
        app'(filter1(x9),x10) -> filter2(x9,x10)
        app'(filter(),x10) -> filter1(x10)
        app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
        app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
        app'(filter21(x9),x10) -> filter22(x9,x10)
        app'(filter2(),x10) -> filter21(x10)
      Qed
    
    DPs:
     minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
     minus{2,#}(minus2(x,y),z) -> minus{2,#}(x,plus2(y,z))
    TRS:
     minus2(x,0()) -> x
     minus2(s1(x),s1(y)) -> minus2(x,y)
     minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
     quot2(0(),s1(y)) -> 0()
     quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
     plus2(0(),y) -> y
     plus2(s1(x),y) -> s1(plus2(x,y))
     app2(nil(),k) -> k
     app2(l,nil()) -> l
     app2(cons2(x,l),k) -> cons2(x,app2(l,k))
     sum1(cons2(x,nil())) -> cons2(x,nil())
     sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
     sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
     map2(f,nil()) -> nil()
     map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app'(minus1(x9),x10) -> minus2(x9,x10)
     app'(minus(),x10) -> minus1(x10)
     app'(s(),x10) -> s1(x10)
     app'(plus1(x9),x10) -> plus2(x9,x10)
     app'(plus(),x10) -> plus1(x10)
     app'(quot1(x9),x10) -> quot2(x9,x10)
     app'(quot(),x10) -> quot1(x10)
     app'(app1(x9),x10) -> app2(x9,x10)
     app'(app(),x10) -> app1(x10)
     app'(cons1(x9),x10) -> cons2(x9,x10)
     app'(cons(),x10) -> cons1(x10)
     app'(sum(),x10) -> sum1(x10)
     app'(map1(x9),x10) -> map2(x9,x10)
     app'(map(),x10) -> map1(x10)
     app'(filter1(x9),x10) -> filter2(x9,x10)
     app'(filter(),x10) -> filter1(x10)
     app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
     app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
     app'(filter21(x9),x10) -> filter22(x9,x10)
     app'(filter2(),x10) -> filter21(x10)
    Subterm Criterion Processor:
     simple projection:
      pi(minus{2,#}) = 0
     problem:
      DPs:
       
      TRS:
       minus2(x,0()) -> x
       minus2(s1(x),s1(y)) -> minus2(x,y)
       minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
       quot2(0(),s1(y)) -> 0()
       quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
       plus2(0(),y) -> y
       plus2(s1(x),y) -> s1(plus2(x,y))
       app2(nil(),k) -> k
       app2(l,nil()) -> l
       app2(cons2(x,l),k) -> cons2(x,app2(l,k))
       sum1(cons2(x,nil())) -> cons2(x,nil())
       sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
       sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
       map2(f,nil()) -> nil()
       map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
       filter2(f,nil()) -> nil()
       filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
       filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
       filter24(false(),f,x,xs) -> filter2(f,xs)
       app'(minus1(x9),x10) -> minus2(x9,x10)
       app'(minus(),x10) -> minus1(x10)
       app'(s(),x10) -> s1(x10)
       app'(plus1(x9),x10) -> plus2(x9,x10)
       app'(plus(),x10) -> plus1(x10)
       app'(quot1(x9),x10) -> quot2(x9,x10)
       app'(quot(),x10) -> quot1(x10)
       app'(app1(x9),x10) -> app2(x9,x10)
       app'(app(),x10) -> app1(x10)
       app'(cons1(x9),x10) -> cons2(x9,x10)
       app'(cons(),x10) -> cons1(x10)
       app'(sum(),x10) -> sum1(x10)
       app'(map1(x9),x10) -> map2(x9,x10)
       app'(map(),x10) -> map1(x10)
       app'(filter1(x9),x10) -> filter2(x9,x10)
       app'(filter(),x10) -> filter1(x10)
       app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
       app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
       app'(filter21(x9),x10) -> filter22(x9,x10)
       app'(filter2(),x10) -> filter21(x10)
     Qed
    
    DPs:
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
    TRS:
     minus2(x,0()) -> x
     minus2(s1(x),s1(y)) -> minus2(x,y)
     minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
     quot2(0(),s1(y)) -> 0()
     quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
     plus2(0(),y) -> y
     plus2(s1(x),y) -> s1(plus2(x,y))
     app2(nil(),k) -> k
     app2(l,nil()) -> l
     app2(cons2(x,l),k) -> cons2(x,app2(l,k))
     sum1(cons2(x,nil())) -> cons2(x,nil())
     sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
     sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
     map2(f,nil()) -> nil()
     map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app'(minus1(x9),x10) -> minus2(x9,x10)
     app'(minus(),x10) -> minus1(x10)
     app'(s(),x10) -> s1(x10)
     app'(plus1(x9),x10) -> plus2(x9,x10)
     app'(plus(),x10) -> plus1(x10)
     app'(quot1(x9),x10) -> quot2(x9,x10)
     app'(quot(),x10) -> quot1(x10)
     app'(app1(x9),x10) -> app2(x9,x10)
     app'(app(),x10) -> app1(x10)
     app'(cons1(x9),x10) -> cons2(x9,x10)
     app'(cons(),x10) -> cons1(x10)
     app'(sum(),x10) -> sum1(x10)
     app'(map1(x9),x10) -> map2(x9,x10)
     app'(map(),x10) -> map1(x10)
     app'(filter1(x9),x10) -> filter2(x9,x10)
     app'(filter(),x10) -> filter1(x10)
     app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
     app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
     app'(filter21(x9),x10) -> filter22(x9,x10)
     app'(filter2(),x10) -> filter21(x10)
    Subterm Criterion Processor:
     simple projection:
      pi(plus{2,#}) = 0
     problem:
      DPs:
       
      TRS:
       minus2(x,0()) -> x
       minus2(s1(x),s1(y)) -> minus2(x,y)
       minus2(minus2(x,y),z) -> minus2(x,plus2(y,z))
       quot2(0(),s1(y)) -> 0()
       quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(y)))
       plus2(0(),y) -> y
       plus2(s1(x),y) -> s1(plus2(x,y))
       app2(nil(),k) -> k
       app2(l,nil()) -> l
       app2(cons2(x,l),k) -> cons2(x,app2(l,k))
       sum1(cons2(x,nil())) -> cons2(x,nil())
       sum1(cons2(x,cons2(y,l))) -> sum1(cons2(plus2(x,y),l))
       sum1(app2(l,cons2(x,cons2(y,k)))) -> sum1(app2(l,sum1(cons2(x,cons2(y,k)))))
       map2(f,nil()) -> nil()
       map2(f,cons2(x,xs)) -> cons2(app'(f,x),map2(f,xs))
       filter2(f,nil()) -> nil()
       filter2(f,cons2(x,xs)) -> filter24(app'(f,x),f,x,xs)
       filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
       filter24(false(),f,x,xs) -> filter2(f,xs)
       app'(minus1(x9),x10) -> minus2(x9,x10)
       app'(minus(),x10) -> minus1(x10)
       app'(s(),x10) -> s1(x10)
       app'(plus1(x9),x10) -> plus2(x9,x10)
       app'(plus(),x10) -> plus1(x10)
       app'(quot1(x9),x10) -> quot2(x9,x10)
       app'(quot(),x10) -> quot1(x10)
       app'(app1(x9),x10) -> app2(x9,x10)
       app'(app(),x10) -> app1(x10)
       app'(cons1(x9),x10) -> cons2(x9,x10)
       app'(cons(),x10) -> cons1(x10)
       app'(sum(),x10) -> sum1(x10)
       app'(map1(x9),x10) -> map2(x9,x10)
       app'(map(),x10) -> map1(x10)
       app'(filter1(x9),x10) -> filter2(x9,x10)
       app'(filter(),x10) -> filter1(x10)
       app'(filter23(x9,x8,x7),x10) -> filter24(x9,x8,x7,x10)
       app'(filter22(x9,x8),x10) -> filter23(x9,x8,x10)
       app'(filter21(x9),x10) -> filter22(x9,x10)
       app'(filter2(),x10) -> filter21(x10)
     Qed