YES
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) -> #(),
     *(0(x), y) -> 0(*(x, y)),
     *(1(x), y) -> +(0(*(x, y)), y),
     *(j(x), y) -> -(0(*(x, y)), y),
  *(*(x, y), z) -> *(x, *(y, z))}
 DP:
  Strict:
   {+#(0(x), 0(y)) -> 0#(+(x, y)),
    +#(0(x), 0(y)) -> +#(x, y),
    +#(0(x), 1(y)) -> +#(x, y),
    +#(0(x), j(y)) -> +#(x, y),
    +#(+(x, y), z) -> +#(x, +(y, z)),
    +#(+(x, y), z) -> +#(y, z),
    +#(1(x), 0(y)) -> +#(x, y),
    +#(1(x), 1(y)) -> +#(x, y),
    +#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
    +#(1(x), j(y)) -> 0#(+(x, y)),
    +#(1(x), j(y)) -> +#(x, y),
    +#(j(x), 0(y)) -> +#(x, y),
    +#(j(x), 1(y)) -> 0#(+(x, y)),
    +#(j(x), 1(y)) -> +#(x, y),
    +#(j(x), j(y)) -> +#(x, y),
    +#(j(x), j(y)) -> +#(+(x, y), j(#())),
        opp#(0(x)) -> 0#(opp(x)),
        opp#(0(x)) -> opp#(x),
        opp#(1(x)) -> opp#(x),
        opp#(j(x)) -> opp#(x),
          -#(x, y) -> +#(x, opp(y)),
          -#(x, y) -> opp#(y),
       *#(0(x), y) -> 0#(*(x, y)),
       *#(0(x), y) -> *#(x, y),
       *#(1(x), y) -> 0#(*(x, y)),
       *#(1(x), y) -> +#(0(*(x, y)), y),
       *#(1(x), y) -> *#(x, y),
       *#(j(x), y) -> 0#(*(x, y)),
       *#(j(x), y) -> -#(0(*(x, y)), y),
       *#(j(x), y) -> *#(x, y),
    *#(*(x, y), z) -> *#(x, *(y, z)),
    *#(*(x, y), z) -> *#(y, z)}
  Weak:
  {       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) -> #(),
      *(0(x), y) -> 0(*(x, y)),
      *(1(x), y) -> +(0(*(x, y)), y),
      *(j(x), y) -> -(0(*(x, y)), y),
   *(*(x, y), z) -> *(x, *(y, z))}
  EDG:
   {
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(j(x), j(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(1(x), j(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(+(x, y), z) -> +#(y, z))
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(j(x), j(y)) -> +#(+(x, y), j(#())), +#(0(x), j(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(0(x), 0(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), j(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(0(x), j(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(0(x), j(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(0(x), j(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), j(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), j(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), j(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), j(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(1(x), 1(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(j(x), 0(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(j(x), 0(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(j(x), 0(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(j(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(j(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(j(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(j(x), 0(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(j(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(j(x), j(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(j(x), j(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(j(x), j(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(j(x), j(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(j(x), j(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(j(x), j(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(j(x), j(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(j(x), j(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(1(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
    (*#(1(x), y) -> *#(x, y), *#(j(x), y) -> -#(0(*(x, y)), y))
    (*#(1(x), y) -> *#(x, y), *#(j(x), y) -> 0#(*(x, y)))
    (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
    (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
    (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
    (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j(x), j(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), j(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), j(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (-#(x, y) -> opp#(y), opp#(j(x)) -> opp#(x))
    (-#(x, y) -> opp#(y), opp#(1(x)) -> opp#(x))
    (-#(x, y) -> opp#(y), opp#(0(x)) -> opp#(x))
    (-#(x, y) -> opp#(y), opp#(0(x)) -> 0#(opp(x)))
    (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
    (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(y, z), *#(j(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(j(x), y) -> -#(0(*(x, y)), y))
    (*#(*(x, y), z) -> *#(y, z), *#(j(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> 0#(*(x, y)))
    (opp#(0(x)) -> opp#(x), opp#(j(x)) -> opp#(x))
    (opp#(0(x)) -> opp#(x), opp#(1(x)) -> opp#(x))
    (opp#(0(x)) -> opp#(x), opp#(0(x)) -> opp#(x))
    (opp#(0(x)) -> opp#(x), opp#(0(x)) -> 0#(opp(x)))
    (opp#(j(x)) -> opp#(x), opp#(j(x)) -> opp#(x))
    (opp#(j(x)) -> opp#(x), opp#(1(x)) -> opp#(x))
    (opp#(j(x)) -> opp#(x), opp#(0(x)) -> opp#(x))
    (opp#(j(x)) -> opp#(x), opp#(0(x)) -> 0#(opp(x)))
    (*#(j(x), y) -> -#(0(*(x, y)), y), -#(x, y) -> opp#(y))
    (*#(j(x), y) -> -#(0(*(x, y)), y), -#(x, y) -> +#(x, opp(y)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 1(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), j(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(y, z))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 0(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), j(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(j(x), 0(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(j(x), 1(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(j(x), j(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (opp#(1(x)) -> opp#(x), opp#(0(x)) -> 0#(opp(x)))
    (opp#(1(x)) -> opp#(x), opp#(0(x)) -> opp#(x))
    (opp#(1(x)) -> opp#(x), opp#(1(x)) -> opp#(x))
    (opp#(1(x)) -> opp#(x), opp#(j(x)) -> opp#(x))
    (-#(x, y) -> +#(x, opp(y)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (-#(x, y) -> +#(x, opp(y)), +#(0(x), 0(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(0(x), 1(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(0(x), j(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (-#(x, y) -> +#(x, opp(y)), +#(+(x, y), z) -> +#(y, z))
    (-#(x, y) -> +#(x, opp(y)), +#(1(x), 0(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(1(x), 1(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (-#(x, y) -> +#(x, opp(y)), +#(1(x), j(y)) -> 0#(+(x, y)))
    (-#(x, y) -> +#(x, opp(y)), +#(1(x), j(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(j(x), 0(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (-#(x, y) -> +#(x, opp(y)), +#(j(x), 1(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(j(x), j(y)) -> +#(x, y))
    (-#(x, y) -> +#(x, opp(y)), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), j(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), j(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(j(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(y, z), +#(j(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(j(x), j(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j(x), y) -> -#(0(*(x, y)), y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
    (*#(j(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
    (*#(j(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
    (*#(j(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
    (*#(j(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(j(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
    (*#(j(x), y) -> *#(x, y), *#(j(x), y) -> 0#(*(x, y)))
    (*#(j(x), y) -> *#(x, y), *#(j(x), y) -> -#(0(*(x, y)), y))
    (*#(j(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
    (*#(j(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(j(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
    (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
    (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
    (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
    (*#(0(x), y) -> *#(x, y), *#(j(x), y) -> 0#(*(x, y)))
    (*#(0(x), y) -> *#(x, y), *#(j(x), y) -> -#(0(*(x, y)), y))
    (*#(0(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
    (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (+#(j(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(j(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(j(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(j(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(j(x), 1(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(j(x), 1(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(j(x), 1(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(j(x), 1(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(1(x), j(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), j(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), j(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), j(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), j(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(1(x), j(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(1(x), j(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(1(x), j(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), j(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), j(y)) -> 0#(+(x, y)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), j(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(j(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(j(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(j(x), j(y)) -> +#(+(x, y), j(#())))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(j(x), 1(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(j(x), 1(y)) -> +#(x, y))
   }
   SCCS:
    Scc:
     {   *#(0(x), y) -> *#(x, y),
         *#(1(x), y) -> *#(x, y),
         *#(j(x), y) -> *#(x, y),
      *#(*(x, y), z) -> *#(x, *(y, z)),
      *#(*(x, y), z) -> *#(y, z)}
    Scc:
     {opp#(0(x)) -> opp#(x),
      opp#(1(x)) -> opp#(x),
      opp#(j(x)) -> opp#(x)}
    Scc:
     {+#(0(x), 0(y)) -> +#(x, y),
      +#(0(x), 1(y)) -> +#(x, y),
      +#(0(x), j(y)) -> +#(x, y),
      +#(+(x, y), z) -> +#(x, +(y, z)),
      +#(+(x, y), z) -> +#(y, z),
      +#(1(x), 0(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
      +#(1(x), j(y)) -> +#(x, y),
      +#(j(x), 0(y)) -> +#(x, y),
      +#(j(x), 1(y)) -> +#(x, y),
      +#(j(x), j(y)) -> +#(x, y),
      +#(j(x), j(y)) -> +#(+(x, y), j(#()))}
    SCC:
     Strict:
      {   *#(0(x), y) -> *#(x, y),
          *#(1(x), y) -> *#(x, y),
          *#(j(x), y) -> *#(x, y),
       *#(*(x, y), z) -> *#(x, *(y, z)),
       *#(*(x, y), z) -> *#(y, z)}
     Weak:
     {       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) -> #(),
         *(0(x), y) -> 0(*(x, y)),
         *(1(x), y) -> +(0(*(x, y)), y),
         *(j(x), y) -> -(0(*(x, y)), y),
      *(*(x, y), z) -> *(x, *(y, z))}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {   *#(0(x), y) -> *#(x, y),
           *#(1(x), y) -> *#(x, y),
           *#(j(x), y) -> *#(x, y),
        *#(*(x, y), z) -> *#(y, z)}
      EDG:
       {(*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
        (*#(0(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
        (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
        (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
        (*#(j(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
        (*#(j(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
        (*#(j(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
        (*#(j(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
        (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
        (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
        (*#(1(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
        (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
        (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y))
        (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> *#(x, y))
        (*#(*(x, y), z) -> *#(y, z), *#(j(x), y) -> *#(x, y))
        (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))}
       SCCS:
        Scc:
         {   *#(0(x), y) -> *#(x, y),
             *#(1(x), y) -> *#(x, y),
             *#(j(x), y) -> *#(x, y),
          *#(*(x, y), z) -> *#(y, z)}
        SCC:
         Strict:
          {   *#(0(x), y) -> *#(x, y),
              *#(1(x), y) -> *#(x, y),
              *#(j(x), y) -> *#(x, y),
           *#(*(x, y), z) -> *#(y, z)}
         Weak:
         {       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) -> #(),
             *(0(x), y) -> 0(*(x, y)),
             *(1(x), y) -> +(0(*(x, y)), y),
             *(j(x), y) -> -(0(*(x, y)), y),
          *(*(x, y), z) -> *(x, *(y, z))}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {*#(0(x), y) -> *#(x, y),
            *#(1(x), y) -> *#(x, y),
            *#(j(x), y) -> *#(x, y)}
          EDG:
           {(*#(1(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
            (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
            (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
            (*#(j(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
            (*#(j(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
            (*#(j(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
            (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
            (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
            (*#(0(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))}
           SCCS:
            Scc:
             {*#(0(x), y) -> *#(x, y),
              *#(1(x), y) -> *#(x, y),
              *#(j(x), y) -> *#(x, y)}
            SCC:
             Strict:
              {*#(0(x), y) -> *#(x, y),
               *#(1(x), y) -> *#(x, y),
               *#(j(x), y) -> *#(x, y)}
             Weak:
             {       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) -> #(),
                 *(0(x), y) -> 0(*(x, y)),
                 *(1(x), y) -> +(0(*(x, y)), y),
                 *(j(x), y) -> -(0(*(x, y)), y),
              *(*(x, y), z) -> *(x, *(y, z))}
             SPSC:
              Simple Projection:
               pi(*#) = 0
              Strict:
               {*#(0(x), y) -> *#(x, y),
                *#(j(x), y) -> *#(x, y)}
              EDG:
               {(*#(j(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))
                (*#(j(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
                (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
                (*#(0(x), y) -> *#(x, y), *#(j(x), y) -> *#(x, y))}
               SCCS:
                Scc:
                 {*#(0(x), y) -> *#(x, y),
                  *#(j(x), y) -> *#(x, y)}
                SCC:
                 Strict:
                  {*#(0(x), y) -> *#(x, y),
                   *#(j(x), y) -> *#(x, y)}
                 Weak:
                 {       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) -> #(),
                     *(0(x), y) -> 0(*(x, y)),
                     *(1(x), y) -> +(0(*(x, y)), y),
                     *(j(x), y) -> -(0(*(x, y)), y),
                  *(*(x, y), z) -> *(x, *(y, z))}
                 SPSC:
                  Simple Projection:
                   pi(*#) = 0
                  Strict:
                   {*#(0(x), y) -> *#(x, y)}
                  EDG:
                   {(*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))}
                   SCCS:
                    Scc:
                     {*#(0(x), y) -> *#(x, y)}
                    SCC:
                     Strict:
                      {*#(0(x), y) -> *#(x, y)}
                     Weak:
                     {       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) -> #(),
                         *(0(x), y) -> 0(*(x, y)),
                         *(1(x), y) -> +(0(*(x, y)), y),
                         *(j(x), y) -> -(0(*(x, y)), y),
                      *(*(x, y), z) -> *(x, *(y, z))}
                     SPSC:
                      Simple Projection:
                       pi(*#) = 0
                      Strict:
                       {}
                      Qed
    SCC:
     Strict:
      {opp#(0(x)) -> opp#(x),
       opp#(1(x)) -> opp#(x),
       opp#(j(x)) -> opp#(x)}
     Weak:
     {       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) -> #(),
         *(0(x), y) -> 0(*(x, y)),
         *(1(x), y) -> +(0(*(x, y)), y),
         *(j(x), y) -> -(0(*(x, y)), y),
      *(*(x, y), z) -> *(x, *(y, z))}
     SPSC:
      Simple Projection:
       pi(opp#) = 0
      Strict:
       {opp#(0(x)) -> opp#(x),
        opp#(j(x)) -> opp#(x)}
      EDG:
       {(opp#(j(x)) -> opp#(x), opp#(j(x)) -> opp#(x))
        (opp#(j(x)) -> opp#(x), opp#(0(x)) -> opp#(x))
        (opp#(0(x)) -> opp#(x), opp#(0(x)) -> opp#(x))
        (opp#(0(x)) -> opp#(x), opp#(j(x)) -> opp#(x))}
       SCCS:
        Scc:
         {opp#(0(x)) -> opp#(x),
          opp#(j(x)) -> opp#(x)}
        SCC:
         Strict:
          {opp#(0(x)) -> opp#(x),
           opp#(j(x)) -> opp#(x)}
         Weak:
         {       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) -> #(),
             *(0(x), y) -> 0(*(x, y)),
             *(1(x), y) -> +(0(*(x, y)), y),
             *(j(x), y) -> -(0(*(x, y)), y),
          *(*(x, y), z) -> *(x, *(y, z))}
         SPSC:
          Simple Projection:
           pi(opp#) = 0
          Strict:
           {opp#(j(x)) -> opp#(x)}
          EDG:
           {(opp#(j(x)) -> opp#(x), opp#(j(x)) -> opp#(x))}
           SCCS:
            Scc:
             {opp#(j(x)) -> opp#(x)}
            SCC:
             Strict:
              {opp#(j(x)) -> opp#(x)}
             Weak:
             {       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) -> #(),
                 *(0(x), y) -> 0(*(x, y)),
                 *(1(x), y) -> +(0(*(x, y)), y),
                 *(j(x), y) -> -(0(*(x, y)), y),
              *(*(x, y), z) -> *(x, *(y, z))}
             SPSC:
              Simple Projection:
               pi(opp#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {+#(0(x), 0(y)) -> +#(x, y),
       +#(0(x), 1(y)) -> +#(x, y),
       +#(0(x), j(y)) -> +#(x, y),
       +#(+(x, y), z) -> +#(x, +(y, z)),
       +#(+(x, y), z) -> +#(y, z),
       +#(1(x), 0(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
       +#(1(x), j(y)) -> +#(x, y),
       +#(j(x), 0(y)) -> +#(x, y),
       +#(j(x), 1(y)) -> +#(x, y),
       +#(j(x), j(y)) -> +#(x, y),
       +#(j(x), j(y)) -> +#(+(x, y), j(#()))}
     Weak:
     {       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) -> #(),
         *(0(x), y) -> 0(*(x, y)),
         *(1(x), y) -> +(0(*(x, y)), y),
         *(j(x), y) -> -(0(*(x, y)), y),
      *(*(x, y), z) -> *(x, *(y, z))}
     POLY:
      Argument Filtering:
       pi(*) = 1, pi(-) = [], pi(opp) = [], pi(j) = [0], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = [0], pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [+#](x0, x1) = x0 + x1,
       [+](x0, x1) = x0 + x1,
       [j](x0) = x0 + 1,
       [1](x0) = x0 + 1,
       [0](x0) = x0 + 1,
       [#] = 0
      Strict:
       {+#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z)}
      Weak:
       {       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) -> #(),
           *(0(x), y) -> 0(*(x, y)),
           *(1(x), y) -> +(0(*(x, y)), y),
           *(j(x), y) -> -(0(*(x, y)), y),
        *(*(x, y), z) -> *(x, *(y, z))}
      EDG:
       {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
        (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))}
       SCCS:
        Scc:
         {+#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z)}
        SCC:
         Strict:
          {+#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z)}
         Weak:
         {       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) -> #(),
             *(0(x), y) -> 0(*(x, y)),
             *(1(x), y) -> +(0(*(x, y)), y),
             *(j(x), y) -> -(0(*(x, y)), y),
          *(*(x, y), z) -> *(x, *(y, z))}
         SPSC:
          Simple Projection:
           pi(+#) = 0
          Strict:
           {+#(+(x, y), z) -> +#(y, z)}
          EDG:
           {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))}
           SCCS:
            Scc:
             {+#(+(x, y), z) -> +#(y, z)}
            SCC:
             Strict:
              {+#(+(x, y), z) -> +#(y, z)}
             Weak:
             {       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) -> #(),
                 *(0(x), y) -> 0(*(x, y)),
                 *(1(x), y) -> +(0(*(x, y)), y),
                 *(j(x), y) -> -(0(*(x, y)), y),
              *(*(x, y), z) -> *(x, *(y, z))}
             SPSC:
              Simple Projection:
               pi(+#) = 0
              Strict:
               {}
              Qed