YES
Time: 0.032964
TRS:
 {      O 0() -> 0(),
    +(x, 0()) -> x,
    +(0(), x) -> x,
  +(O x, O y) -> O +(x, y),
  +(O x, I y) -> I +(x, y),
  +(I x, O y) -> I +(x, y),
  +(I x, I y) -> O +(+(x, y), I 0()),
    *(x, 0()) -> 0(),
    *(0(), x) -> 0(),
    *(O x, y) -> O *(x, y),
    *(I x, y) -> +(O *(x, y), y)}
 DP:
  DP:
   {+#(O x, O y) -> O# +(x, y),
    +#(O x, O y) -> +#(x, y),
    +#(O x, I y) -> +#(x, y),
    +#(I x, O y) -> +#(x, y),
    +#(I x, I y) -> O# +(+(x, y), I 0()),
    +#(I x, I y) -> +#(x, y),
    +#(I x, I y) -> +#(+(x, y), I 0()),
      *#(O x, y) -> O# *(x, y),
      *#(O x, y) -> *#(x, y),
      *#(I x, y) -> O# *(x, y),
      *#(I x, y) -> +#(O *(x, y), y),
      *#(I x, y) -> *#(x, y)}
  TRS:
  {      O 0() -> 0(),
     +(x, 0()) -> x,
     +(0(), x) -> x,
   +(O x, O y) -> O +(x, y),
   +(O x, I y) -> I +(x, y),
   +(I x, O y) -> I +(x, y),
   +(I x, I y) -> O +(+(x, y), I 0()),
     *(x, 0()) -> 0(),
     *(0(), x) -> 0(),
     *(O x, y) -> O *(x, y),
     *(I x, y) -> +(O *(x, y), y)}
  EDG:
   {(+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
    (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
    (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(O x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
    (+#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
    (+#(O x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
    (+#(O x, O y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
    (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
    (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(I x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
    (+#(I x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
    (+#(I x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
    (+#(I x, O y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (*#(O x, y) -> *#(x, y), *#(I x, y) -> *#(x, y))
    (*#(O x, y) -> *#(x, y), *#(I x, y) -> +#(O *(x, y), y))
    (*#(O x, y) -> *#(x, y), *#(I x, y) -> O# *(x, y))
    (*#(O x, y) -> *#(x, y), *#(O x, y) -> *#(x, y))
    (*#(O x, y) -> *#(x, y), *#(O x, y) -> O# *(x, y))
    (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(+(x, y), I 0()))
    (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(x, y))
    (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, I y) -> +#(x, y))
    (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> +#(+(x, y), I 0()))
    (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> +#(x, y))
    (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (*#(I x, y) -> +#(O *(x, y), y), +#(I x, O y) -> +#(x, y))
    (*#(I x, y) -> +#(O *(x, y), y), +#(O x, I y) -> +#(x, y))
    (*#(I x, y) -> +#(O *(x, y), y), +#(O x, O y) -> +#(x, y))
    (*#(I x, y) -> +#(O *(x, y), y), +#(O x, O y) -> O# +(x, y))
    (*#(I x, y) -> *#(x, y), *#(O x, y) -> O# *(x, y))
    (*#(I x, y) -> *#(x, y), *#(O x, y) -> *#(x, y))
    (*#(I x, y) -> *#(x, y), *#(I x, y) -> O# *(x, y))
    (*#(I x, y) -> *#(x, y), *#(I x, y) -> +#(O *(x, y), y))
    (*#(I x, y) -> *#(x, y), *#(I x, y) -> *#(x, y))
    (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
    (+#(I x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
    (+#(I x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
    (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
    (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
    (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
    (+#(O x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
    (+#(O x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
    (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
    (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))}
   SCCS (2):
    Scc:
     {*#(O x, y) -> *#(x, y),
      *#(I x, y) -> *#(x, y)}
    Scc:
     {+#(O x, O y) -> +#(x, y),
      +#(O x, I y) -> +#(x, y),
      +#(I x, O y) -> +#(x, y),
      +#(I x, I y) -> +#(x, y),
      +#(I x, I y) -> +#(+(x, y), I 0())}
    SCC (2):
     Strict:
      {*#(O x, y) -> *#(x, y),
       *#(I x, y) -> *#(x, y)}
     Weak:
     {      O 0() -> 0(),
        +(x, 0()) -> x,
        +(0(), x) -> x,
      +(O x, O y) -> O +(x, y),
      +(O x, I y) -> I +(x, y),
      +(I x, O y) -> I +(x, y),
      +(I x, I y) -> O +(+(x, y), I 0()),
        *(x, 0()) -> 0(),
        *(0(), x) -> 0(),
        *(O x, y) -> O *(x, y),
        *(I x, y) -> +(O *(x, y), y)}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {*#(I x, y) -> *#(x, y)}
      EDG:
       {(*#(I x, y) -> *#(x, y), *#(I x, y) -> *#(x, y))}
       SCCS (1):
        Scc:
         {*#(I x, y) -> *#(x, y)}
        SCC (1):
         Strict:
          {*#(I x, y) -> *#(x, y)}
         Weak:
         {      O 0() -> 0(),
            +(x, 0()) -> x,
            +(0(), x) -> x,
          +(O x, O y) -> O +(x, y),
          +(O x, I y) -> I +(x, y),
          +(I x, O y) -> I +(x, y),
          +(I x, I y) -> O +(+(x, y), I 0()),
            *(x, 0()) -> 0(),
            *(0(), x) -> 0(),
            *(O x, y) -> O *(x, y),
            *(I x, y) -> +(O *(x, y), y)}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {}
          Qed
    SCC (5):
     Strict:
      {+#(O x, O y) -> +#(x, y),
       +#(O x, I y) -> +#(x, y),
       +#(I x, O y) -> +#(x, y),
       +#(I x, I y) -> +#(x, y),
       +#(I x, I y) -> +#(+(x, y), I 0())}
     Weak:
     {      O 0() -> 0(),
        +(x, 0()) -> x,
        +(0(), x) -> x,
      +(O x, O y) -> O +(x, y),
      +(O x, I y) -> I +(x, y),
      +(I x, O y) -> I +(x, y),
      +(I x, I y) -> O +(+(x, y), I 0()),
        *(x, 0()) -> 0(),
        *(0(), x) -> 0(),
        *(O x, y) -> O *(x, y),
        *(I x, y) -> +(O *(x, y), y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [+](x0, x1) = x0 + x1,
       
       [*](x0, x1) = x0 + 1,
       
       [O](x0) = x0 + 1,
       
       [I](x0) = x0 + 1,
       
       [0] = 0,
       
       [+#](x0, x1) = x0 + x1
      Strict:
       +#(I x, I y) -> +#(+(x, y), I 0())
       2 + 1x + 1y >= 1 + 1x + 1y
       +#(I x, I y) -> +#(x, y)
       2 + 1x + 1y >= 0 + 1x + 1y
       +#(I x, O y) -> +#(x, y)
       2 + 1x + 1y >= 0 + 1x + 1y
       +#(O x, I y) -> +#(x, y)
       2 + 1x + 1y >= 0 + 1x + 1y
       +#(O x, O y) -> +#(x, y)
       2 + 1x + 1y >= 0 + 1x + 1y
      Weak:
       
     Qed