YES Problem: 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)) Proof: Uncurry Processor: map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) app(map1(x3),x4) -> map2(x3,x4) app(map(),x4) -> map1(x4) app(cons1(x3),x4) -> cons2(x3,x4) app(cons(),x4) -> cons1(x4) DP Processor: DPs: map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(map1(x3),x4) -> map{2,#}(x3,x4) TRS: map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) app(map1(x3),x4) -> map2(x3,x4) app(map(),x4) -> map1(x4) app(cons1(x3),x4) -> cons2(x3,x4) app(cons(),x4) -> cons1(x4) TDG Processor: DPs: map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(map1(x3),x4) -> map{2,#}(x3,x4) TRS: map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) app(map1(x3),x4) -> map2(x3,x4) app(map(),x4) -> map1(x4) app(cons1(x3),x4) -> cons2(x3,x4) app(cons(),x4) -> cons1(x4) graph: app#(map1(x3),x4) -> map{2,#}(x3,x4) -> map{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(map1(x3),x4) -> map{2,#}(x3,x4) -> map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(map1(x3),x4) -> map{2,#}(x3,x4) map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) -> map{2,#}(f,cons2(x,xs)) -> app#(f,x) map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) -> map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) Subterm Criterion Processor: simple projection: pi(map{2,#}) = 1 pi(app#) = 1 problem: DPs: app#(map1(x3),x4) -> map{2,#}(x3,x4) TRS: map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) app(map1(x3),x4) -> map2(x3,x4) app(map(),x4) -> map1(x4) app(cons1(x3),x4) -> cons2(x3,x4) app(cons(),x4) -> cons1(x4) SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/1