YES

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

Proof:
 Bounds Processor:
  bound: 1
  enrichment: roof
  automaton:
   final states: {7,4}
   transitions:
    minus0(7) -> 7*,4
    minus0(4) -> 7*,4
    minux0(7) -> 7*,4
    minux0(4) -> 7*,4
    +0(4,4) -> 7*,4
    +0(7,7) -> 7*,4
    +0(4,7) -> 7*,4
    +0(7,4) -> 7*,4
    +1(4,4) -> 7*,4
    +1(7,5) -> 7*,4
    +1(7,7) -> 7*,4
    +1(4,7) -> 7*,4
    +1(6,5) -> 7*,4
    +1(6,7) -> 7*,4
    +1(7,4) -> 7*,4
    minus1(5) -> 7*,4
    minus1(7) -> 7*,4
    minus1(4) -> 6,5,7*,4
    minus1(6) -> 7*,4
    4 -> 7*
    5 -> 4*
    6 -> 4*
    7 -> 4*
  problem:
   
  Qed