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)),
             *(x, h()) -> h(),
         *(s(x), s(y)) -> s(+(+(*(x, y), x), y)),
             *(h(), x) -> h()
 }
 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)),
               *(x, h()) -> h(),
           *(s(x), s(y)) -> s(+(+(*(x, y), x), y)),
               *(h(), x) -> h()
   }
  Fail