YES

Problem:
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 +(p(x),y) -> p(+(x,y))
 minus(0()) -> 0()
 minus(s(x)) -> p(minus(x))
 minus(p(x)) -> s(minus(x))
 *(0(),y) -> 0()
 *(s(x),y) -> +(*(x,y),y)
 *(p(x),y) -> +(*(x,y),minus(y))

Proof:
 DP Processor:
  DPs:
   +#(s(x),y) -> +#(x,y)
   +#(p(x),y) -> +#(x,y)
   minus#(s(x)) -> minus#(x)
   minus#(p(x)) -> minus#(x)
   *#(s(x),y) -> *#(x,y)
   *#(s(x),y) -> +#(*(x,y),y)
   *#(p(x),y) -> minus#(y)
   *#(p(x),y) -> *#(x,y)
   *#(p(x),y) -> +#(*(x,y),minus(y))
  TRS:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   +(p(x),y) -> p(+(x,y))
   minus(0()) -> 0()
   minus(s(x)) -> p(minus(x))
   minus(p(x)) -> s(minus(x))
   *(0(),y) -> 0()
   *(s(x),y) -> +(*(x,y),y)
   *(p(x),y) -> +(*(x,y),minus(y))
  TDG Processor:
   DPs:
    +#(s(x),y) -> +#(x,y)
    +#(p(x),y) -> +#(x,y)
    minus#(s(x)) -> minus#(x)
    minus#(p(x)) -> minus#(x)
    *#(s(x),y) -> *#(x,y)
    *#(s(x),y) -> +#(*(x,y),y)
    *#(p(x),y) -> minus#(y)
    *#(p(x),y) -> *#(x,y)
    *#(p(x),y) -> +#(*(x,y),minus(y))
   TRS:
    +(0(),y) -> y
    +(s(x),y) -> s(+(x,y))
    +(p(x),y) -> p(+(x,y))
    minus(0()) -> 0()
    minus(s(x)) -> p(minus(x))
    minus(p(x)) -> s(minus(x))
    *(0(),y) -> 0()
    *(s(x),y) -> +(*(x,y),y)
    *(p(x),y) -> +(*(x,y),minus(y))
   graph:
    *#(p(x),y) -> *#(x,y) -> *#(p(x),y) -> +#(*(x,y),minus(y))
    *#(p(x),y) -> *#(x,y) -> *#(p(x),y) -> *#(x,y)
    *#(p(x),y) -> *#(x,y) -> *#(p(x),y) -> minus#(y)
    *#(p(x),y) -> *#(x,y) -> *#(s(x),y) -> +#(*(x,y),y)
    *#(p(x),y) -> *#(x,y) -> *#(s(x),y) -> *#(x,y)
    *#(p(x),y) -> minus#(y) -> minus#(p(x)) -> minus#(x)
    *#(p(x),y) -> minus#(y) -> minus#(s(x)) -> minus#(x)
    *#(p(x),y) -> +#(*(x,y),minus(y)) -> +#(p(x),y) -> +#(x,y)
    *#(p(x),y) -> +#(*(x,y),minus(y)) -> +#(s(x),y) -> +#(x,y)
    *#(s(x),y) -> *#(x,y) -> *#(p(x),y) -> +#(*(x,y),minus(y))
    *#(s(x),y) -> *#(x,y) -> *#(p(x),y) -> *#(x,y)
    *#(s(x),y) -> *#(x,y) -> *#(p(x),y) -> minus#(y)
    *#(s(x),y) -> *#(x,y) -> *#(s(x),y) -> +#(*(x,y),y)
    *#(s(x),y) -> *#(x,y) -> *#(s(x),y) -> *#(x,y)
    *#(s(x),y) -> +#(*(x,y),y) -> +#(p(x),y) -> +#(x,y)
    *#(s(x),y) -> +#(*(x,y),y) -> +#(s(x),y) -> +#(x,y)
    minus#(p(x)) -> minus#(x) -> minus#(p(x)) -> minus#(x)
    minus#(p(x)) -> minus#(x) -> minus#(s(x)) -> minus#(x)
    minus#(s(x)) -> minus#(x) -> minus#(p(x)) -> minus#(x)
    minus#(s(x)) -> minus#(x) -> minus#(s(x)) -> minus#(x)
    +#(p(x),y) -> +#(x,y) -> +#(p(x),y) -> +#(x,y)
    +#(p(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
    +#(s(x),y) -> +#(x,y) -> +#(p(x),y) -> +#(x,y)
    +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 6
    #arcs: 24/81
    DPs:
     *#(p(x),y) -> *#(x,y)
     *#(s(x),y) -> *#(x,y)
    TRS:
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     +(p(x),y) -> p(+(x,y))
     minus(0()) -> 0()
     minus(s(x)) -> p(minus(x))
     minus(p(x)) -> s(minus(x))
     *(0(),y) -> 0()
     *(s(x),y) -> +(*(x,y),y)
     *(p(x),y) -> +(*(x,y),minus(y))
    LPO Processor:
     argument filtering:
      pi(0) = []
      pi(+) = [0,1]
      pi(s) = [0]
      pi(p) = [0]
      pi(minus) = [0]
      pi(*) = [0,1]
      pi(*#) = 0
     precedence:
      * > minus > + > *# ~ p ~ s ~ 0
     problem:
      DPs:
       
      TRS:
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       +(p(x),y) -> p(+(x,y))
       minus(0()) -> 0()
       minus(s(x)) -> p(minus(x))
       minus(p(x)) -> s(minus(x))
       *(0(),y) -> 0()
       *(s(x),y) -> +(*(x,y),y)
       *(p(x),y) -> +(*(x,y),minus(y))
     Qed
    
    DPs:
     minus#(s(x)) -> minus#(x)
     minus#(p(x)) -> minus#(x)
    TRS:
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     +(p(x),y) -> p(+(x,y))
     minus(0()) -> 0()
     minus(s(x)) -> p(minus(x))
     minus(p(x)) -> s(minus(x))
     *(0(),y) -> 0()
     *(s(x),y) -> +(*(x,y),y)
     *(p(x),y) -> +(*(x,y),minus(y))
    LPO Processor:
     argument filtering:
      pi(0) = []
      pi(+) = [0,1]
      pi(s) = [0]
      pi(p) = [0]
      pi(minus) = [0]
      pi(*) = [0,1]
      pi(minus#) = 0
     precedence:
      * > minus > + > minus# ~ p ~ s ~ 0
     problem:
      DPs:
       
      TRS:
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       +(p(x),y) -> p(+(x,y))
       minus(0()) -> 0()
       minus(s(x)) -> p(minus(x))
       minus(p(x)) -> s(minus(x))
       *(0(),y) -> 0()
       *(s(x),y) -> +(*(x,y),y)
       *(p(x),y) -> +(*(x,y),minus(y))
     Qed
    
    DPs:
     +#(s(x),y) -> +#(x,y)
     +#(p(x),y) -> +#(x,y)
    TRS:
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     +(p(x),y) -> p(+(x,y))
     minus(0()) -> 0()
     minus(s(x)) -> p(minus(x))
     minus(p(x)) -> s(minus(x))
     *(0(),y) -> 0()
     *(s(x),y) -> +(*(x,y),y)
     *(p(x),y) -> +(*(x,y),minus(y))
    LPO Processor:
     argument filtering:
      pi(0) = []
      pi(+) = [0,1]
      pi(s) = [0]
      pi(p) = [0]
      pi(minus) = [0]
      pi(*) = [0,1]
      pi(+#) = 0
     precedence:
      * > + > minus > +# ~ p ~ s ~ 0
     problem:
      DPs:
       
      TRS:
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       +(p(x),y) -> p(+(x,y))
       minus(0()) -> 0()
       minus(s(x)) -> p(minus(x))
       minus(p(x)) -> s(minus(x))
       *(0(),y) -> 0()
       *(s(x),y) -> +(*(x,y),y)
       *(p(x),y) -> +(*(x,y),minus(y))
     Qed