MAYBE
Trs:
 { a(h(), h(), h(), x) -> s(x),
  a(s(l), h(), h(), z) -> a(l, z, h(), z),
    a(l, s(x), h(), z) -> a(l, x, z, z),
    a(l, x, s(y), h()) -> a(l, x, y, s(h())),
   a(l, x, s(y), s(z)) -> a(l, x, y, a(l, x, s(y), z)),
             *(h(), x) -> h(),
         *(s(x), s(y)) -> s(+(+(*(x, y), x), y)),
             *(x, h()) -> h(),
             +(h(), x) -> x,
         +(+(x, y), z) -> +(x, +(y, z)),
         +(s(x), s(y)) -> s(s(+(x, y))),
             +(x, h()) -> x,
                s(h()) -> 1()}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open