MAYBE 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(D(),app(minus(),x)) -> app(minus(),app(D(),x)) app(D(),app(app(div(),x),y)) -> app(app(-(),app(app(div(),app(D(),x)),y)),app(app(div(),app(app(*(),x),app(D(),y))), app(app(pow(),y),2()))) app(D(),app(ln(),x)) -> app(app(div(),app(D(),x)),x) app(D(),app(app(pow(),x),y)) -> app(app(+(),app(app(*(),app(app(*(),y),app(app(pow(),x),app(app(-(),y),1())))),app(D(),x))), app(app(*(),app(app(*(),app(app(pow(),x),y)),app(ln(),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#(D(),app(minus(),x)) -> app#(D(),x) app#(D(),app(minus(),x)) -> app#(minus(),app(D(),x)) app#(D(),app(app(div(),x),y)) -> app#(pow(),y) app#(D(),app(app(div(),x),y)) -> app#(app(pow(),y),2()) app#(D(),app(app(div(),x),y)) -> app#(D(),y) app#(D(),app(app(div(),x),y)) -> app#(*(),x) app#(D(),app(app(div(),x),y)) -> app#(app(*(),x),app(D(),y)) app#(D(),app(app(div(),x),y)) -> app#(div(),app(app(*(),x),app(D(),y))) app#(D(),app(app(div(),x),y)) -> app#(app(div(),app(app(*(),x),app(D(),y))),app(app(pow(),y),2())) app#(D(),app(app(div(),x),y)) -> app#(D(),x) app#(D(),app(app(div(),x),y)) -> app#(div(),app(D(),x)) app#(D(),app(app(div(),x),y)) -> app#(app(div(),app(D(),x)),y) app#(D(),app(app(div(),x),y)) -> app#(-(),app(app(div(),app(D(),x)),y)) app#(D(),app(app(div(),x),y)) -> app#(app(-(),app(app(div(),app(D(),x)),y)),app(app(div(),app(app(*(),x),app(D(),y))), app(app(pow(),y),2()))) app#(D(),app(ln(),x)) -> app#(D(),x) app#(D(),app(ln(),x)) -> app#(div(),app(D(),x)) app#(D(),app(ln(),x)) -> app#(app(div(),app(D(),x)),x) app#(D(),app(app(pow(),x),y)) -> app#(D(),y) app#(D(),app(app(pow(),x),y)) -> app#(ln(),x) app#(D(),app(app(pow(),x),y)) -> app#(*(),app(app(pow(),x),y)) app#(D(),app(app(pow(),x),y)) -> app#(app(*(),app(app(pow(),x),y)),app(ln(),x)) app#(D(),app(app(pow(),x),y)) -> app#(*(),app(app(*(),app(app(pow(),x),y)),app(ln(),x))) app#(D(),app(app(pow(),x),y)) -> app#(app(*(),app(app(*(),app(app(pow(),x),y)),app(ln(),x))),app(D(),y)) app#(D(),app(app(pow(),x),y)) -> app#(D(),x) app#(D(),app(app(pow(),x),y)) -> app#(-(),y) app#(D(),app(app(pow(),x),y)) -> app#(app(-(),y),1()) app#(D(),app(app(pow(),x),y)) -> app#(app(pow(),x),app(app(-(),y),1())) app#(D(),app(app(pow(),x),y)) -> app#(*(),y) app#(D(),app(app(pow(),x),y)) -> app#(app(*(),y),app(app(pow(),x),app(app(-(),y),1()))) app#(D(),app(app(pow(),x),y)) -> app#(*(),app(app(*(),y),app(app(pow(),x),app(app(-(),y),1())))) app#(D(),app(app(pow(),x),y)) -> app#(app(*(),app(app(*(),y),app(app(pow(),x),app(app(-(),y),1())))),app(D(),x)) app#(D(),app(app(pow(),x),y)) -> app#(+(),app(app(*(),app(app(*(),y),app(app(pow(),x),app(app(-(),y),1())))),app(D(),x))) app#(D(),app(app(pow(),x),y)) -> app#(app(+(),app(app(*(),app(app(*(),y),app(app(pow(),x),app(app(-(),y),1())))),app(D(),x))), app(app(*(),app(app(*(),app(app(pow(),x),y)),app(ln(),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(D(),app(minus(),x)) -> app(minus(),app(D(),x)) app(D(),app(app(div(),x),y)) -> app(app(-(),app(app(div(),app(D(),x)),y)),app(app(div(),app(app(*(),x),app(D(),y))), app(app(pow(),y),2()))) app(D(),app(ln(),x)) -> app(app(div(),app(D(),x)),x) app(D(),app(app(pow(),x),y)) -> app(app(+(),app(app(*(),app(app(*(),y),app(app(pow(),x),app(app(-(),y),1())))),app(D(),x))), app(app(*(),app(app(*(),app(app(pow(),x),y)),app(ln(),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) Open