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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   
  critical peaks: 1
  -(0()) <-1|0[]- -(+(x(),-(x()))) -0|[]-> 0()
  Shift Processor lab=left (dd):
   
   strict:
    -(+(x(),-(x()))) -> -(0())
    -(+(x(),-(x()))) -> 0()
    0() -> -(0())
   weak:
    -(+(x(),-(x()))) -> 0()
    +(x(),-(x())) -> 0()
    0() -> -(0())
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5,6}
     transitions:
      -1(5) -> 5*
      01() -> 5*
      -0(5) -> 5*
      -0(6) -> 5*
      +0(5,5) -> 5*
      +0(6,6) -> 5*
      +0(5,6) -> 5*
      +0(6,5) -> 5*
      x0() -> 6*
      00() -> 5*
    problem:
     
     strict:
      -(+(x(),-(x()))) -> -(0())
      0() -> -(0())
     weak:
      -(+(x(),-(x()))) -> 0()
      +(x(),-(x())) -> 0()
      0() -> -(0())
    Bounds Processor:
     bound: 1
     enrichment: match-rt
     automaton:
      final states: {5,6}
      transitions:
       -1(8) -> 8,5
       01() -> 8*
       -0(5) -> 5*
       -0(6) -> 5*
       +0(5,5) -> 5*
       +0(6,6) -> 5*
       +0(5,6) -> 5*
       +0(6,5) -> 5*
       x0() -> 6*
       00() -> 5*
     problem:
      
      strict:
       0() -> -(0())
      weak:
       -(+(x(),-(x()))) -> 0()
       +(x(),-(x())) -> 0()
       0() -> -(0())
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [0] = 0,
       
       [+](x0, x1) = 2x0 + x1 + 3,
       
       [-](x0) = 4x0,
       
       [x] = 0
      orientation:
       0() = 0 >= 0 = -(0())
       
       -(+(x(),-(x()))) = 12 >= 0 = 0()
       
       +(x(),-(x())) = 3 >= 0 = 0()
      problem:
       
       strict:
        0() -> -(0())
       weak:
        0() -> -(0())
      Shift Processor (ldh) lab=left (force):
       
       strict:
        
       weak:
        
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         -(0()) <-1|0[1]- -(+(x(),-(x()))) -0|[1]-> 0()
        joins:
         
         0() -2|[0]-> -(0())
        Qed