MAYBE

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:
 DP Processor:
  DPs:
   app'#(app'(minus(),app'(s(),x)),app'(s(),y)) -> app'#(minus(),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'#(plus(),y)
   app'#(app'(minus(),app'(app'(minus(),x),y)),z) -> app'#(app'(plus(),y),z)
   app'#(app'(minus(),app'(app'(minus(),x),y)),z) -> app'#(app'(minus(),x),app'(app'(plus(),y),z))
   app'#(app'(quot(),app'(s(),x)),app'(s(),y)) -> app'#(minus(),x)
   app'#(app'(quot(),app'(s(),x)),app'(s(),y)) -> app'#(app'(minus(),x),y)
   app'#(app'(quot(),app'(s(),x)),app'(s(),y)) -> app'#(quot(),app'(app'(minus(),x),y))
   app'#(app'(quot(),app'(s(),x)),app'(s(),y)) ->
   app'#(app'(quot(),app'(app'(minus(),x),y)),app'(s(),y))
   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(),app'(s(),x)),y) -> app'#(plus(),x)
   app'#(app'(plus(),app'(s(),x)),y) -> app'#(app'(plus(),x),y)
   app'#(app'(plus(),app'(s(),x)),y) -> app'#(s(),app'(app'(plus(),x),y))
   app'#(app'(app(),app'(app'(cons(),x),l)),k) -> app'#(app(),l)
   app'#(app'(app(),app'(app'(cons(),x),l)),k) -> app'#(app'(app(),l),k)
   app'#(app'(app(),app'(app'(cons(),x),l)),k) -> app'#(app'(cons(),x),app'(app'(app(),l),k))
   app'#(sum(),app'(app'(cons(),x),app'(app'(cons(),y),l))) -> app'#(plus(),x)
   app'#(sum(),app'(app'(cons(),x),app'(app'(cons(),y),l))) -> app'#(app'(plus(),x),y)
   app'#(sum(),app'(app'(cons(),x),app'(app'(cons(),y),l))) -> app'#(cons(),app'(app'(plus(),x),y))
   app'#(sum(),app'(app'(cons(),x),app'(app'(cons(),y),l))) ->
   app'#(app'(cons(),app'(app'(plus(),x),y)),l)
   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'(cons(),x),app'(app'(cons(),y),k)))
   app'#(sum(),app'(app'(app(),l),app'(app'(cons(),x),app'(app'(cons(),y),k)))) ->
   app'#(app'(app(),l),app'(sum(),app'(app'(cons(),x),app'(app'(cons(),y),k))))
   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),app'(app'(cons(),x),xs)) -> app'#(app'(map(),f),xs)
   app'#(app'(map(),f),app'(app'(cons(),x),xs)) -> app'#(f,x)
   app'#(app'(map(),f),app'(app'(cons(),x),xs)) -> app'#(cons(),app'(f,x))
   app'#(app'(map(),f),app'(app'(cons(),x),xs)) ->
   app'#(app'(cons(),app'(f,x)),app'(app'(map(),f),xs))
   app'#(app'(filter(),f),app'(app'(cons(),x),xs)) -> app'#(f,x)
   app'#(app'(filter(),f),app'(app'(cons(),x),xs)) -> app'#(filter2(),app'(f,x))
   app'#(app'(filter(),f),app'(app'(cons(),x),xs)) -> app'#(app'(filter2(),app'(f,x)),f)
   app'#(app'(filter(),f),app'(app'(cons(),x),xs)) -> app'#(app'(app'(filter2(),app'(f,x)),f),x)
   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'#(filter(),f)
   app'#(app'(app'(app'(filter2(),true()),f),x),xs) -> app'#(app'(filter(),f),xs)
   app'#(app'(app'(app'(filter2(),true()),f),x),xs) -> app'#(cons(),x)
   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'#(filter(),f)
   app'#(app'(app'(app'(filter2(),false()),f),x),xs) -> app'#(app'(filter(),f),xs)
  TRS:
   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)
  Open