YES Problem: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Proof: DP Processor: DPs: app#(f(),app(s(),x)) -> app#(f(),x) app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) app#(h(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),x),y)) app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(cons(),app(fun,x)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(filter(),fun) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(cons(),x) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(cons(),x),app(app(filter(),fun),xs)) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(filter(),fun) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) EDG Processor: DPs: app#(f(),app(s(),x)) -> app#(f(),x) app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) app#(h(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),x),y)) app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(cons(),app(fun,x)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(filter(),fun) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(cons(),x) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(cons(),x),app(app(filter(),fun),xs)) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(filter(),fun) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) graph: app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) -> app#(h(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),x),y)) app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) -> app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) app#(h(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) -> app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(f(),app(s(),x)) -> app#(f(),x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(h(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),x),y)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(cons(),app(fun,x)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(filter(),fun) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(cons(),x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(cons(),x),app(app(filter(),fun),xs)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(filter(),fun) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(cons(),app(fun,x)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(f(),app(s(),x)) -> app#(f(),x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(h(),app(app(cons(),x),y)) -> app#(g(),app(app(cons(),x),y)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(cons(),app(fun,x)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(filter(),fun) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(cons(),x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(cons(),x),app(app(filter(),fun),xs)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(filter(),fun) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) -> app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) -> app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(f(),app(s(),x)) -> app#(f(),x) -> app#(f(),app(s(),x)) -> app#(f(),x) SCC Processor: #sccs: 4 #rules: 8 #arcs: 57/361 DPs: app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) SCC Processor: #sccs: 0 #rules: 0 #arcs: 14/4 DPs: app#(f(),app(s(),x)) -> app#(f(),x) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Qed DPs: app#(h(),app(app(cons(),x),y)) -> app#(h(),app(g(),app(app(cons(),x),y))) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Arctic Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = 1x0 + x1 + 0, [false] = 4, [true] = 2, [filter2] = 4, [filter] = 4, [nil] = 2, [map] = 2, [h] = 0, [0] = 2, [cons] = 2, [g] = 0, [app](x0, x1) = x0 + 0, [s] = 0, [f] = 2 orientation: app#(h(),app(app(cons(),x),y)) = 2 >= 1 = app#(h(),app(g(),app(app(cons(),x),y))) app(f(),app(s(),x)) = 2 >= 2 = app(f(),x) app(g(),app(app(cons(),0()),y)) = 0 >= 0 = app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) = 0 >= 0 = app(s(),x) app(h(),app(app(cons(),x),y)) = 0 >= 0 = app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) = 2 >= 2 = nil() app(app(map(),fun),app(app(cons(),x),xs)) = 2 >= 2 = app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) = 4 >= 2 = nil() app(app(filter(),fun),app(app(cons(),x),xs)) = 4 >= 4 = app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) = 4 >= 2 = app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) = 4 >= 4 = app(app(filter(),fun),xs) problem: DPs: TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Qed DPs: app#(g(),app(app(cons(),0()),y)) -> app#(g(),y) TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: app(f(),app(s(),x)) -> app(f(),x) app(g(),app(app(cons(),0()),y)) -> app(g(),y) app(g(),app(app(cons(),app(s(),x)),y)) -> app(s(),x) app(h(),app(app(cons(),x),y)) -> app(h(),app(g(),app(app(cons(),x),y))) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Qed