NO

1 decompositions
 #1 -----------
   4: minus(x3,0()) -> x3
   5: minus(x4,p(x5)) -> s(minus(x4,x5))
   6: minus(x6,s(x7)) -> p(minus(x6,x7))
   7: minus(0(),x8) -> inv(x8)
   8: minus(s(x9),s(x10)) -> minus(x9,x10)
   9: minus(p(x11),p(x12)) -> minus(x11,x12)
  10: inv(x13) -> minus(0(),x13)
  11: s(p(x14)) -> x14
  12: p(s(x15)) -> x15

unjoinable peak
    s(minus(p(x37),x38))
*<- minus(p(x37),p(x38)) ->*
    minus(x37,x38)
NOTE: input TRS is reduced

original is
   1: inv(0()) -> 0()
   2: inv(s(x1)) -> p(inv(x1))
   3: inv(p(x2)) -> s(inv(x2))
   4: minus(x3,0()) -> x3
   5: minus(x4,p(x5)) -> s(minus(x4,x5))
   6: minus(x6,s(x7)) -> p(minus(x6,x7))
   7: minus(0(),x8) -> inv(x8)
   8: minus(s(x9),s(x10)) -> minus(x9,x10)
   9: minus(p(x11),p(x12)) -> minus(x11,x12)
  10: inv(x13) -> minus(0(),x13)
  11: s(p(x14)) -> x14
  12: p(s(x15)) -> x15

reduced to
   4: minus(x3,0()) -> x3
   5: minus(x4,p(x5)) -> s(minus(x4,x5))
   6: minus(x6,s(x7)) -> p(minus(x6,x7))
   7: minus(0(),x8) -> inv(x8)
   8: minus(s(x9),s(x10)) -> minus(x9,x10)
   9: minus(p(x11),p(x12)) -> minus(x11,x12)
  10: inv(x13) -> minus(0(),x13)
  11: s(p(x14)) -> x14
  12: p(s(x15)) -> x15