YES Problem: app(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),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(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),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(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),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#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),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(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#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),y)) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(-(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(*(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),y)) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(D(),y) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),y)) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(+(),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(+(),x),y)) -> app#(app(+(),app(D(),x)),app(D(),y)) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(*(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(*(),y),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(+(),app(app(*(),y),app(D(),x))) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(*(),x),y)) -> app#(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(-(),app(D(),x)) app#(D(),app(app(+(),x),y)) -> app#(D(),x) -> app#(D(),app(app(-(),x),y)) -> app#(app(-(),app(D(),x)),app(D(),y)) SCC Processor: #sccs: 2 #rules: 11 #arcs: 164/900 DPs: 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(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(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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: 14/4 DPs: app#(D(),app(app(-(),x),y)) -> app#(D(),x) app#(D(),app(app(-(),x),y)) -> app#(D(),y) app#(D(),app(app(*(),x),y)) -> app#(D(),x) app#(D(),app(app(*(),x),y)) -> app#(D(),y) app#(D(),app(app(+(),x),y)) -> app#(D(),x) app#(D(),app(app(+(),x),y)) -> app#(D(),y) TRS: app(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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(D(),t()) -> 1() app(D(),constant()) -> 0() app(D(),app(app(+(),x),y)) -> app(app(+(),app(D(),x)),app(D(),y)) app(D(),app(app(*(),x),y)) -> app(app(+(),app(app(*(),y),app(D(),x))),app(app(*(),x),app(D(),y))) app(D(),app(app(-(),x),y)) -> app(app(-(),app(D(),x)),app(D(),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