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