Problem:
 -(+(x(),-(x()))) -> 0()
 +(x(),-(x())) -> 0()
 0() -> -(0())

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   0() -> -(0())
   +(x(),-(x())) -> 0()
   -(+(x(),-(x()))) -> 0()
  weak:
   
  critical peaks: 1
   -(0()) <-1|0[]- -(+(x(),-(x()))) -2|[]-> 0()
  Closedness Processor (*strongly -- <=7 steps*):
   
   Qed