MAYBE Problem: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) Proof: DP Processor: DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),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)) TRS: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) EDG Processor: DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),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)) TRS: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) 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(add(),app(s(),x)),y) -> app#(add(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),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(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) CDG Processor: DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),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)) TRS: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) 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(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#(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(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) SCC Processor: #sccs: 2 #rules: 3 #arcs: 14/49 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) TRS: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) Qed DPs: app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) TRS: app(id(),x) -> x app(add(),0()) -> id() app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),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)) Open