MAYBE
MAYBE
TRS:
 {
                    s(h()) -> 1(),
       a(l, x, s(y), s(z)) -> a(l, x, y, a(l, x, s(y), z)),
        a(l, x, s(y), h()) -> a(l, x, y, s(h())),
        a(l, s(x), h(), z) -> a(l, x, z, z),
      a(s(l), h(), h(), z) -> a(l, z, h(), z),
       a(h(), h(), h(), x) -> s(x),
                 +(x, h()) -> x,
             +(s(x), s(y)) -> s(s(+(x, y))),
                 +(h(), x) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
             app(l, nil()) -> l,
             app(nil(), k) -> k,
        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(a(x, y, h(), h()), l))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                      s(h()) -> 1(),
         a(l, x, s(y), s(z)) -> a(l, x, y, a(l, x, s(y), z)),
          a(l, x, s(y), h()) -> a(l, x, y, s(h())),
          a(l, s(x), h(), z) -> a(l, x, z, z),
        a(s(l), h(), h(), z) -> a(l, z, h(), z),
         a(h(), h(), h(), x) -> s(x),
                   +(x, h()) -> x,
               +(s(x), s(y)) -> s(s(+(x, y))),
                   +(h(), x) -> x,
               +(+(x, y), z) -> +(x, +(y, z)),
               app(l, nil()) -> l,
               app(nil(), k) -> k,
          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(a(x, y, h(), h()), l))
   }
  Fail