YES Problem: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) Proof: DP Processor: DPs: app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(cons(),y),app(app(filter(),f),ys)) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) TRS: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) CDG Processor: DPs: app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(cons(),y),app(app(filter(),f),ys)) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) TRS: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) graph: app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y)) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y)) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(cons(),y),app(app(filter(),f),ys)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) -> app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) Restore Modifier: DPs: app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y)) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(cons(),y),app(app(filter(),f),ys)) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f) app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) TRS: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) SCC Processor: #sccs: 1 #rules: 3 #arcs: 17/81 DPs: app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) TRS: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0 + 1, [false] = 0, [true] = 0, [filtersub] = 0, [cons] = 0, [nil] = 0, [app](x0, x1) = x1 + 1, [filter] = 0 orientation: app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) = f + 2 >= f + 2 = app#(app(filter(),f),ys) app#(app(filter(),f),app(app(cons(),y),ys)) = f + 2 >= f + 1 = app#(f,y) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) = f + 2 >= f + 2 = app#(app(filter(),f),ys) app(app(filter(),f),nil()) = 1 >= 0 = nil() app(app(filter(),f),app(app(cons(),y),ys)) = ys + 2 >= ys + 2 = app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) = ys + 2 >= ys + 2 = app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) = ys + 2 >= ys + 1 = app(app(filter(),f),ys) problem: DPs: app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) TRS: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x1, [false] = 0, [true] = 0, [filtersub] = 0, [cons] = 0, [nil] = 1, [app](x0, x1) = x1 + 1, [filter] = 0 orientation: app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) = ys + 1 >= ys = app#(app(filter(),f),ys) app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) = ys + 1 >= ys = app#(app(filter(),f),ys) app(app(filter(),f),nil()) = 2 >= 1 = nil() app(app(filter(),f),app(app(cons(),y),ys)) = ys + 2 >= ys + 2 = app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) = ys + 2 >= ys + 2 = app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) = ys + 2 >= ys + 1 = app(app(filter(),f),ys) problem: DPs: TRS: app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),y),ys)) -> app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app(app(cons(),y),app(app(filter(),f),ys)) app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys) Qed