MAYBE Problem: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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#(double(),app(s(),x)) -> app#(double(),x) app#(double(),app(s(),x)) -> app#(s(),app(double(),x)) app#(double(),app(s(),x)) -> app#(s(),app(s(),app(double(),x))) 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(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) EDG 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#(double(),app(s(),x)) -> app#(double(),x) app#(double(),app(s(),x)) -> app#(s(),app(double(),x)) app#(double(),app(s(),x)) -> app#(s(),app(s(),app(double(),x))) 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(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) graph: app#(double(),app(s(),x)) -> app#(double(),x) -> app#(double(),app(s(),x)) -> app#(double(),x) app#(double(),app(s(),x)) -> app#(double(),x) -> app#(double(),app(s(),x)) -> app#(s(),app(double(),x)) app#(double(),app(s(),x)) -> app#(double(),x) -> app#(double(),app(s(),x)) -> app#(s(),app(s(),app(double(),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(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(filter(),f),xs) 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#(cons(),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#(app(cons(),x),app(app(filter(),f),xs)) 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(),false()),f),x),xs) -> app#(filter(),f) 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(),false()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(minus(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(app(minus(),x),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),app(s(),x)) -> app#(double(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),app(s(),x)) -> app#(s(),app(double(),x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),app(s(),x)) -> app#(s(),app(s(),app(double(),x))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(filter(),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(filter(),f),app(app(cons(),x),xs)) -> 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#(f,x) 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#(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#(f,x) -> 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#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) 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#(app(map(),f),xs) -> 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(map(),f),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(minus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(app(minus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),app(s(),x)) -> app#(double(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),app(s(),x)) -> app#(s(),app(double(),x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),app(s(),x)) -> app#(s(),app(s(),app(double(),x))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> 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#(f,x) 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#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),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(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(plus(),app(s(),x)),y) -> app#(double(),y) -> app#(double(),app(s(),x)) -> app#(double(),x) app#(app(plus(),app(s(),x)),y) -> app#(double(),y) -> app#(double(),app(s(),x)) -> app#(s(),app(double(),x)) app#(app(plus(),app(s(),x)),y) -> app#(double(),y) -> app#(double(),app(s(),x)) -> app#(s(),app(s(),app(double(),x))) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),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#(app(plus(),x),y) 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(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(double(),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(minus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),app(app(minus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) -> app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(minus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(minus(),x),y) -> app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(app(minus(),x),y) app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x)) app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f) app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x) app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) -> 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(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x)) app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f) app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x) app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs) app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(app(minus(),x),y) -> 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(s(),x)),app(s(),y)) -> app#(app(minus(),x),y) SCC Processor: #sccs: 4 #rules: 11 #arcs: 125/961 DPs: 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(),false()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) TRS: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) app#(app(app(app(filter2(),true()),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(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) SCC Processor: #sccs: 0 #rules: 0 #arcs: 20/4 DPs: app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),app(app(minus(),x),y)),app(double(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),app(s(),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) TRS: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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 DPs: app#(app(minus(),app(s(),x)),app(s(),y)) -> app#(app(minus(),x),y) TRS: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) Qed DPs: app#(double(),app(s(),x)) -> app#(double(),x) TRS: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: app(app(minus(),x),0()) -> x app(app(minus(),app(s(),x)),app(s(),y)) -> app(app(minus(),x),y) app(double(),0()) -> 0() app(double(),app(s(),x)) -> app(s(),app(s(),app(double(),x))) app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(plus(),app(s(),x)),y) -> app(app(plus(),x),app(s(),y)) app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),app(app(minus(),x),y)),app(double(),y))) 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) Qed