MAYBE

Problem:
 a(h(),h(),h(),x) -> s(x)
 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))
 a(l,s(x),h(),z) -> a(l,x,z,z)
 a(s(l),h(),h(),z) -> a(l,z,h(),z)
 +(x,h()) -> x
 +(h(),x) -> x
 +(s(x),s(y)) -> s(s(+(x,y)))
 +(+(x,y),z) -> +(x,+(y,z))
 s(h()) -> 1()
 *(h(),x) -> h()
 *(x,h()) -> h()
 *(s(x),s(y)) -> s(+(+(*(x,y),x),y))

Proof:
 DP Processor:
  DPs:
   a#(h(),h(),h(),x) -> s#(x)
   a#(l,x,s(y),h()) -> s#(h())
   a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
   a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
   a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
   a#(l,s(x),h(),z) -> a#(l,x,z,z)
   a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
   +#(s(x),s(y)) -> +#(x,y)
   +#(s(x),s(y)) -> s#(+(x,y))
   +#(s(x),s(y)) -> s#(s(+(x,y)))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   *#(s(x),s(y)) -> *#(x,y)
   *#(s(x),s(y)) -> +#(*(x,y),x)
   *#(s(x),s(y)) -> +#(+(*(x,y),x),y)
   *#(s(x),s(y)) -> s#(+(+(*(x,y),x),y))
  TRS:
   a(h(),h(),h(),x) -> s(x)
   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))
   a(l,s(x),h(),z) -> a(l,x,z,z)
   a(s(l),h(),h(),z) -> a(l,z,h(),z)
   +(x,h()) -> x
   +(h(),x) -> x
   +(s(x),s(y)) -> s(s(+(x,y)))
   +(+(x,y),z) -> +(x,+(y,z))
   s(h()) -> 1()
   *(h(),x) -> h()
   *(x,h()) -> h()
   *(s(x),s(y)) -> s(+(+(*(x,y),x),y))
  Open