YES Problem: app(app(app(if(),true()),x),y) -> x app(app(app(if(),false()),x),y) -> y app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) Proof: DP Processor: DPs: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(cons(),x),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(if(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) TRS: app(app(app(if(),true()),x),y) -> x app(app(app(if(),false()),x),y) -> y app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) EDG Processor: DPs: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(cons(),x),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(if(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) TRS: app(app(app(if(),true()),x),y) -> x app(app(app(if(),false()),x),y) -> y app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) graph: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(cons(),x),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(if(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(cons(),x),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(if(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 12/36 DPs: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) TRS: app(app(app(if(),true()),x),y) -> x app(app(app(if(),false()),x),y) -> y app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))),app(app(filter(),f),xs)) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: TRS: app(app(app(if(),true()),x),y) -> x app(app(app(if(),false()),x),y) -> y app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(if(),app(f,x)),app(app(cons(),x),app(app(filter(),f),xs))), app(app(filter(),f),xs)) Qed