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)) app(app(treemap(),f),app(app(node(),x),xs)) -> app(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) Proof: DP Processor: 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(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(treemap(),f),app(app(node(),x),xs)) -> app#(map(),app(treemap(),f)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(node(),app(f,x)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) TRS: 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(treemap(),f),app(app(node(),x),xs)) -> app(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) EDG Processor: 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(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(treemap(),f),app(app(node(),x),xs)) -> app#(map(),app(treemap(),f)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(node(),app(f,x)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) TRS: 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(treemap(),f),app(app(node(),x),xs)) -> app(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) graph: app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(treemap(),f),app(app(node(),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(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(map(),app(treemap(),f)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(node(),app(f,x)) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(node(),app(f,x)),app(app(map(),app(treemap(),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(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(treemap(),f),app(app(node(),x),xs)) -> app#(map(),app(treemap(),f)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(node(),app(f,x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) SCC Processor: #sccs: 1 #rules: 4 #arcs: 26/81 DPs: app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(app(map(),app(treemap(),f)),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(treemap(),f),app(app(node(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) TRS: 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(treemap(),f),app(app(node(),x),xs)) -> app(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: 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(treemap(),f),app(app(node(),x),xs)) -> app(app(node(),app(f,x)),app(app(map(),app(treemap(),f)),xs)) Qed