MAYBE
MAYBE
TRS:
 {
                        app(l, nil()) -> l,
                        app(nil(), k) -> k,
                   app(cons(x, l), k) -> cons(x, app(l, k)),
     sum(app(l, cons(x, cons(y, k)))) ->
  sum(app(l, sum(cons(x, cons(y, k))))),
                  sum(cons(x, nil())) -> cons(x, nil()),
             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)))),
                         plus(0(), y) -> y,
                        plus(s(x), y) -> s(plus(x, y)),
              pred(cons(s(x), nil())) -> cons(x, nil())
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
       sum(app(l, cons(x, cons(y, k)))) ->
    sum(app(l, sum(cons(x, cons(y, k))))),
                    sum(cons(x, nil())) -> cons(x, nil()),
               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)))),
                           plus(0(), y) -> y,
                          plus(s(x), y) -> s(plus(x, y)),
                pred(cons(s(x), nil())) -> cons(x, nil())
   }
  Fail