YES Problem: app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) Proof: DP Processor: DPs: app#(app(app(consif(),true()),x),ys) -> app#(cons(),x) app#(app(app(consif(),true()),x),ys) -> app#(app(cons(),x),ys) 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#(consif(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(consif(),app(f,x)),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) TRS: app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) CDG Processor: DPs: app#(app(app(consif(),true()),x),ys) -> app#(cons(),x) app#(app(app(consif(),true()),x),ys) -> app#(app(cons(),x),ys) 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#(consif(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(consif(),app(f,x)),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) TRS: app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),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#(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#(consif(),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(consif(),app(f,x)),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(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) -> app#(app(app(consif(),true()),x),ys) -> app#(cons(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) -> app#(app(app(consif(),true()),x),ys) -> app#(app(cons(),x),ys) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(consif(),true()),x),ys) -> app#(cons(),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(app(consif(),true()),x),ys) -> app#(app(cons(),x),ys) 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#(f,x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(consif(),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(consif(),app(f,x)),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) Restore Modifier: DPs: app#(app(app(consif(),true()),x),ys) -> app#(cons(),x) app#(app(app(consif(),true()),x),ys) -> app#(app(cons(),x),ys) 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#(consif(),app(f,x)) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(consif(),app(f,x)),x) app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) TRS: app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 14/49 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(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0 + 1, [nil] = 0, [filter] = 0, [false] = 0, [cons] = 0, [app](x0, x1) = x1 + 1, [true] = 0, [consif] = 0 orientation: app#(app(filter(),f),app(app(cons(),x),xs)) = f + 2 >= f + 2 = app#(app(filter(),f),xs) app#(app(filter(),f),app(app(cons(),x),xs)) = f + 2 >= f + 1 = app#(f,x) app(app(app(consif(),true()),x),ys) = ys + 1 >= ys + 1 = app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) = ys + 1 >= ys = ys app(app(filter(),f),nil()) = 1 >= 0 = nil() app(app(filter(),f),app(app(cons(),x),xs)) = xs + 2 >= xs + 2 = app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) problem: DPs: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter(),f),xs) TRS: app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x1 + 1, [nil] = 1, [filter] = 0, [false] = 0, [cons] = 0, [app](x0, x1) = x1 + 1, [true] = 0, [consif] = 0 orientation: app#(app(filter(),f),app(app(cons(),x),xs)) = xs + 2 >= xs + 1 = app#(app(filter(),f),xs) app(app(app(consif(),true()),x),ys) = ys + 1 >= ys + 1 = app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) = ys + 1 >= ys = ys app(app(filter(),f),nil()) = 2 >= 1 = nil() app(app(filter(),f),app(app(cons(),x),xs)) = xs + 2 >= xs + 2 = app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) problem: DPs: TRS: app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys) app(app(app(consif(),false()),x),ys) -> ys app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs)) Qed