MAYBE
MAYBE
TRS:
 {
         0(#()) -> #(),
      +(x, #()) -> x,
      +(#(), x) -> x,
  +(0(x), 0(y)) -> 0(+(x, y)),
  +(0(x), 1(y)) -> 1(+(x, y)),
  +(0(x), j(y)) -> j(+(x, y)),
  +(+(x, y), z) -> +(x, +(y, z)),
  +(1(x), 0(y)) -> 1(+(x, y)),
  +(1(x), 1(y)) -> j(+(+(x, y), 1(#()))),
  +(1(x), j(y)) -> 0(+(x, y)),
  +(j(x), 0(y)) -> j(+(x, y)),
  +(j(x), 1(y)) -> 0(+(x, y)),
  +(j(x), j(y)) -> 1(+(+(x, y), j(#()))),
       opp(#()) -> #(),
      opp(0(x)) -> 0(opp(x)),
      opp(1(x)) -> j(opp(x)),
      opp(j(x)) -> 1(opp(x)),
        -(x, y) -> +(x, opp(y)),
  *(x, +(y, z)) -> +(*(x, y), *(x, z)),
      *(#(), x) -> #(),
     *(0(x), y) -> 0(*(x, y)),
  *(+(x, y), z) -> +(*(x, z), *(y, z)),
     *(1(x), y) -> +(0(*(x, y)), y),
     *(j(x), y) -> -(0(*(x, y)), y),
  *(*(x, y), z) -> *(x, *(y, z))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
           0(#()) -> #(),
        +(x, #()) -> x,
        +(#(), x) -> x,
    +(0(x), 0(y)) -> 0(+(x, y)),
    +(0(x), 1(y)) -> 1(+(x, y)),
    +(0(x), j(y)) -> j(+(x, y)),
    +(+(x, y), z) -> +(x, +(y, z)),
    +(1(x), 0(y)) -> 1(+(x, y)),
    +(1(x), 1(y)) -> j(+(+(x, y), 1(#()))),
    +(1(x), j(y)) -> 0(+(x, y)),
    +(j(x), 0(y)) -> j(+(x, y)),
    +(j(x), 1(y)) -> 0(+(x, y)),
    +(j(x), j(y)) -> 1(+(+(x, y), j(#()))),
         opp(#()) -> #(),
        opp(0(x)) -> 0(opp(x)),
        opp(1(x)) -> j(opp(x)),
        opp(j(x)) -> 1(opp(x)),
          -(x, y) -> +(x, opp(y)),
    *(x, +(y, z)) -> +(*(x, y), *(x, z)),
        *(#(), x) -> #(),
       *(0(x), y) -> 0(*(x, y)),
    *(+(x, y), z) -> +(*(x, z), *(y, z)),
       *(1(x), y) -> +(0(*(x, y)), y),
       *(j(x), y) -> -(0(*(x, y)), y),
    *(*(x, y), z) -> *(x, *(y, z))
   }
  Fail