YES Problem: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Proof: DP Processor: DPs: app#(cons(x,l),k) -> app#(l,k) sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) plus#(s(x),y) -> plus#(x,y) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Usable Rule Processor: DPs: app#(cons(x,l),k) -> app#(l,k) sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) plus#(s(x),y) -> plus#(x,y) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) TRS: plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) TDG Processor: DPs: app#(cons(x,l),k) -> app#(l,k) sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) plus#(s(x),y) -> plus#(x,y) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) TRS: plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) graph: plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) -> sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(cons(x,cons(y,l))) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) -> sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) -> sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) -> sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) -> app#(cons(x,l),k) -> app#(l,k) app#(cons(x,l),k) -> app#(l,k) -> app#(cons(x,l),k) -> app#(l,k) Restore Modifier: DPs: app#(cons(x,l),k) -> app#(l,k) sum#(cons(x,cons(y,l))) -> plus#(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) plus#(s(x),y) -> plus#(x,y) sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l)))) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) SCC Processor: #sccs: 3 #rules: 6 #arcs: 32/81 DPs: sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [sum#](x0) = x0, [pred](x0) = 0, [s](x0) = x0, [0] = 0, [plus](x0, x1) = x1, [sum](x0) = 0, [cons](x0, x1) = 0, [app](x0, x1) = x0 + x1 + 1, [nil] = 0 orientation: sum#(plus(cons(0(),x),cons(y,l))) = 0 >= 0 = sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) = 0 >= 0 = sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) = l + 1 >= 0 = sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) = l + 1 >= l + 1 = sum#(app(l,sum(cons(x,cons(y,k))))) app(nil(),k) = k + 1 >= k = k app(l,nil()) = l + 1 >= l = l app(cons(x,l),k) = k + 1 >= 0 = cons(x,app(l,k)) sum(cons(x,nil())) = 0 >= 0 = cons(x,nil()) sum(cons(x,cons(y,l))) = 0 >= 0 = sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) = 0 >= 0 = sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) = y >= y = y plus(s(x),y) = y >= y = s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) = 0 >= 0 = pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) = 0 >= 0 = cons(x,nil()) problem: DPs: sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [sum#](x0) = x0, [pred](x0) = x0, [s](x0) = x0 + 1, [0] = 1, [plus](x0, x1) = x0 + x1, [sum](x0) = x0, [cons](x0, x1) = x0 + x1 + 1, [app](x0, x1) = x0 + x1, [nil] = 1 orientation: sum#(plus(cons(0(),x),cons(y,l))) = l + x + y + 3 >= l + x + y + 3 = sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) = l + x + y + 2 >= l + x + y + 1 = sum#(cons(plus(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) = k + l + x + y + 2 >= k + l + x + y + 2 = sum#(app(l,sum(cons(x,cons(y,k))))) app(nil(),k) = k + 1 >= k = k app(l,nil()) = l + 1 >= l = l app(cons(x,l),k) = k + l + x + 1 >= k + l + x + 1 = cons(x,app(l,k)) sum(cons(x,nil())) = x + 2 >= x + 2 = cons(x,nil()) sum(cons(x,cons(y,l))) = l + x + y + 2 >= l + x + y + 1 = sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 2 >= k + l + x + y + 2 = sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) = y + 1 >= y = y plus(s(x),y) = x + y + 1 >= x + y + 1 = s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) = l + x + y + 3 >= l + x + y + 3 = pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) = x + 3 >= x + 2 = cons(x,nil()) problem: DPs: sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [sum#](x0) = x0, [pred](x0) = x0, [s](x0) = 1, [0] = 0, [plus](x0, x1) = x0 + x1, [sum](x0) = 1, [cons](x0, x1) = x1 + 1, [app](x0, x1) = x0 + x1, [nil] = 0 orientation: sum#(plus(cons(0(),x),cons(y,l))) = l + x + 2 >= l + 2 = sum#(cons(s(x),cons(y,l))) sum#(app(l,cons(x,cons(y,k)))) = k + l + 2 >= l + 1 = sum#(app(l,sum(cons(x,cons(y,k))))) app(nil(),k) = k >= k = k app(l,nil()) = l >= l = l app(cons(x,l),k) = k + l + 1 >= k + l + 1 = cons(x,app(l,k)) sum(cons(x,nil())) = 1 >= 1 = cons(x,nil()) sum(cons(x,cons(y,l))) = 1 >= 1 = sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) = 1 >= 1 = sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) = y >= y = y plus(s(x),y) = y + 1 >= 1 = s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) = 1 >= 1 = pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) = 1 >= 1 = cons(x,nil()) problem: DPs: sum#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l))) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [sum#](x0) = x0, [pred](x0) = 0, [s](x0) = x0, [0] = 0, [plus](x0, x1) = x1 + 1, [sum](x0) = 0, [cons](x0, x1) = x1, [app](x0, x1) = x0 + x1, [nil] = 0 orientation: sum#(plus(cons(0(),x),cons(y,l))) = l + 1 >= l = sum#(cons(s(x),cons(y,l))) app(nil(),k) = k >= k = k app(l,nil()) = l >= l = l app(cons(x,l),k) = k + l >= k + l = cons(x,app(l,k)) sum(cons(x,nil())) = 0 >= 0 = cons(x,nil()) sum(cons(x,cons(y,l))) = 0 >= 0 = sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) = 0 >= 0 = sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) = y + 1 >= y = y plus(s(x),y) = y + 1 >= y + 1 = s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) = 0 >= 0 = pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) = 0 >= 0 = cons(x,nil()) problem: DPs: TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Qed DPs: app#(cons(x,l),k) -> app#(l,k) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0 + 1, [pred](x0) = 1, [s](x0) = x0, [0] = 0, [plus](x0, x1) = x1 + 1, [sum](x0) = 1, [cons](x0, x1) = x1 + 1, [app](x0, x1) = x0 + x1 + 1, [nil] = 0 orientation: app#(cons(x,l),k) = l + 2 >= l + 1 = app#(l,k) app(nil(),k) = k + 1 >= k = k app(l,nil()) = l + 1 >= l = l app(cons(x,l),k) = k + l + 2 >= k + l + 2 = cons(x,app(l,k)) sum(cons(x,nil())) = 1 >= 1 = cons(x,nil()) sum(cons(x,cons(y,l))) = 1 >= 1 = sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) = 1 >= 1 = sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) = y + 1 >= y = y plus(s(x),y) = y + 1 >= y + 1 = s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) = 1 >= 1 = pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) = 1 >= 1 = cons(x,nil()) problem: DPs: TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Qed DPs: plus#(s(x),y) -> plus#(x,y) TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [plus#](x0, x1) = x0 + 1, [pred](x0) = 0, [s](x0) = x0 + 1, [0] = 0, [plus](x0, x1) = x0 + x1, [sum](x0) = 0, [cons](x0, x1) = 0, [app](x0, x1) = x0 + x1, [nil] = 0 orientation: plus#(s(x),y) = x + 2 >= x + 1 = plus#(x,y) app(nil(),k) = k >= k = k app(l,nil()) = l >= l = l app(cons(x,l),k) = k >= 0 = cons(x,app(l,k)) sum(cons(x,nil())) = 0 >= 0 = cons(x,nil()) sum(cons(x,cons(y,l))) = 0 >= 0 = sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) = 0 >= 0 = sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) = y >= y = y plus(s(x),y) = x + y + 1 >= x + y + 1 = s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) = 0 >= 0 = pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) = 0 >= 0 = cons(x,nil()) problem: DPs: TRS: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l)))) pred(cons(s(x),nil())) -> cons(x,nil()) Qed