YES

We show the termination of the TRS R:

  minus(minus(x)) -> x
  minux(+(x,y)) -> +(minus(y),minus(x))
  +(minus(x),+(x,y)) -> y
  +(+(x,y),minus(y)) -> x

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: minux#(+(x,y)) -> +#(minus(y),minus(x))
p2: minux#(+(x,y)) -> minus#(y)
p3: minux#(+(x,y)) -> minus#(x)

and R consists of:

r1: minus(minus(x)) -> x
r2: minux(+(x,y)) -> +(minus(y),minus(x))
r3: +(minus(x),+(x,y)) -> y
r4: +(+(x,y),minus(y)) -> x

The estimated dependency graph contains the following SCCs:

  (no SCCs)