MAYBE Problem: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),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(app(curry(),g),x),y) -> app(app(g,x),y) inc() -> app(map(),app(app(curry(),plus()),app(s(),0()))) Proof: DP Processor: DPs: 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(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(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(s(),0()) inc#() -> app#(curry(),plus()) inc#() -> app#(app(curry(),plus()),app(s(),0())) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),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(app(curry(),g),x),y) -> app(app(g,x),y) inc() -> app(map(),app(app(curry(),plus()),app(s(),0()))) TDG Processor: DPs: 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(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(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(s(),0()) inc#() -> app#(curry(),plus()) inc#() -> app#(app(curry(),plus()),app(s(),0())) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),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(app(curry(),g),x),y) -> app(app(g,x),y) inc() -> app(map(),app(app(curry(),plus()),app(s(),0()))) graph: inc#() -> app#(curry(),plus()) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(curry(),plus()) -> app#(app(app(curry(),g),x),y) -> app#(g,x) inc#() -> app#(curry(),plus()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) inc#() -> app#(curry(),plus()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) inc#() -> app#(curry(),plus()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) inc#() -> app#(curry(),plus()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) inc#() -> app#(curry(),plus()) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) inc#() -> app#(curry(),plus()) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) inc#() -> app#(curry(),plus()) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(app(curry(),g),x),y) -> app#(g,x) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) inc#() -> app#(s(),0()) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(s(),0()) -> app#(app(app(curry(),g),x),y) -> app#(g,x) inc#() -> app#(s(),0()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) inc#() -> app#(s(),0()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) inc#() -> app#(s(),0()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) inc#() -> app#(s(),0()) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) inc#() -> app#(s(),0()) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) inc#() -> app#(s(),0()) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) inc#() -> app#(s(),0()) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(app(curry(),g),x),y) -> app#(g,x) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) inc#() -> app#(app(curry(),plus()),app(s(),0())) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) -> app#(app(app(curry(),g),x),y) -> app#(g,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(map(),f),app(app(cons(),x),xs)) -> app#(cons(),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#(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#(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#(cons(),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#(cons(),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#(cons(),app(f,x)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) -> app#(app(app(curry(),g),x),y) -> app#(g,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#(app(cons(),app(f,x)),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#(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(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#(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(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(app(curry(),g),x),y) -> app#(g,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#(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#(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(map(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(curry(),g),x),y) -> app#(g,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(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#(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(map(),f),xs) 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#(app(plus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) -> app#(app(app(curry(),g),x),y) -> app#(g,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#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),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(),app(app(plus(),x),y)) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(plus(),app(s(),x)),y) -> app#(s(),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(),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#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(app(curry(),g),x),y) -> app#(g,x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),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#(app(plus(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) 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#(app(plus(),x),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#(plus(),x) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(app(curry(),g),x),y) -> app#(g,x) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),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#(plus(),x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),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#(plus(),x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) EDG Processor: DPs: 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(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(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) inc#() -> app#(s(),0()) inc#() -> app#(curry(),plus()) inc#() -> app#(app(curry(),plus()),app(s(),0())) inc#() -> app#(map(),app(app(curry(),plus()),app(s(),0()))) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),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(app(curry(),g),x),y) -> app(app(g,x),y) inc() -> app(map(),app(app(curry(),plus()),app(s(),0()))) graph: 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(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(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(app(curry(),g),x),y) -> app#(g,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(app(curry(),g),x),y) -> app#(g,x) app#(app(app(curry(),g),x),y) -> app#(g,x) -> app#(app(app(curry(),g),x),y) -> app#(app(g,x),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)) SCC Processor: #sccs: 2 #rules: 5 #arcs: 34/169 DPs: 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(app(curry(),g),x),y) -> app#(app(g,x),y) app#(app(app(curry(),g),x),y) -> app#(g,x) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),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(app(curry(),g),x),y) -> app(app(g,x),y) inc() -> app(map(),app(app(curry(),plus()),app(s(),0()))) Open DPs: app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),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(app(curry(),g),x),y) -> app(app(g,x),y) inc() -> app(map(),app(app(curry(),plus()),app(s(),0()))) Open