MAYBE

Problem:
 ++(++(x,y),z) -> ++(x,++(y,z))
 ++(x,++(y,z)) -> ++(++(x,y),z)
 ++(0(),x) -> x
 +(x,y) -> +(y,x)
 +(+(x,y),z) -> +(x,+(y,z))
 +(0(),x) -> x
 +(s(x),y) -> s(+(x,y))

Proof:
 sorted: (order)
 0:+(x,y) -> +(y,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(0(),x) -> x
   +(s(x),y) -> s(+(x,y))
 1:++(++(x,y),z) -> ++(x,++(y,z))
   ++(x,++(y,z)) -> ++(++(x,y),z)
   ++(0(),x) -> x
 -----
 sorts
   [0>2, 1>2]
 sort attachment (non-strict)
   ++ : 1 x 1 -> 1
   0 : 2
   + : 0 x 0 -> 0
   s : 0 -> 0
 -----
 0:+(x,y) -> +(y,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(0(),x) -> x
   +(s(x),y) -> s(+(x,y))
   AT confluence processor
    Complete TRS T' of input TRS:
    +(0(),x) -> x
    +(s(x),y) -> s(+(x,y))
    +(x,0()) -> x
    +(x,s(x50)) -> s(+(x,x50))
    +(x,y) -> +(y,x)
    +(+(x,y),z) -> +(x,+(y,z))
    
     T' = (P union S) with
    
     TRS P:+(x,y) -> +(y,x)
           +(+(x,y),z) -> +(x,+(y,z))
    
     TRS S:+(0(),x) -> x
           +(s(x),y) -> s(+(x,y))
           +(x,0()) -> x
           +(x,s(x50)) -> s(+(x,x50))
    
    S is left-linear and P is reversible.
    
     CP(S,S) = 
    0() = 0(), s(x50) = s(+(0(),x50)), s(+(x272,0())) = s(x272), s(+(x274,s(x50))) = 
    s(+(s(x274),x50)), s(x) = s(+(x,0())), s(+(0(),x279)) = s(x279), 
    s(+(s(x),x281)) = s(+(x,s(x281)))
    
     CP(S,P union P^-1) = 
    y = +(y,0()), +(y,z) = +(0(),+(y,z)), x = +(x,0()), +(y,z) = +(+(0(),y),z), 
    +(x,z) = +(+(x,0()),z), s(+(x323,y)) = +(y,s(x323)), +(s(+(x325,y)),z) = 
    +(s(x325),+(y,z)), s(+(x327,x)) = +(x,s(x327)), s(+(x329,+(y,z))) = 
    +(+(s(x329),y),z), +(x,s(+(x331,z))) = +(+(x,s(x331)),z), x = +(0(),x), 
    +(x,y) = +(x,+(y,0())), +(x,z) = +(x,+(0(),z)), y = +(0(),y), +(x,y) = 
    +(+(x,y),0()), s(+(x,x339)) = +(s(x339),x), s(+(+(x,y),x341)) = +(x,+(y,s(x341))), 
    +(s(+(x,x343)),z) = +(x,+(s(x343),z)), s(+(y,x345)) = +(s(x345),y), 
    +(x,s(+(y,x347))) = +(+(x,y),s(x347))
    
    
     PCP_in(P union P^-1,S) = 
    
    
    We have to check termination of S:
    
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [s](x0) = x0,
      
      [+](x0, x1) = 2x0 + x1 + 5,
      
      [0] = 4
     orientation:
      +(0(),x) = x + 13 >= x = x
      
      +(s(x),y) = 2x + y + 5 >= 2x + y + 5 = s(+(x,y))
      
      +(x,0()) = 2x + 9 >= x = x
      
      +(x,s(x50)) = 2x + x50 + 5 >= 2x + x50 + 5 = s(+(x,x50))
     problem:
      +(s(x),y) -> s(+(x,y))
      +(x,s(x50)) -> s(+(x,x50))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [s](x0) = x0 + 1,
       
       [+](x0, x1) = 4x0 + x1
      orientation:
       +(s(x),y) = 4x + y + 4 >= 4x + y + 1 = s(+(x,y))
       
       +(x,s(x50)) = 4x + x50 + 1 >= 4x + x50 + 1 = s(+(x,x50))
      problem:
       +(x,s(x50)) -> s(+(x,x50))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [s](x0) = x0 + 1,
        
        [+](x0, x1) = x0 + 2x1 + 5
       orientation:
        +(x,s(x50)) = x + 2x50 + 7 >= x + 2x50 + 6 = s(+(x,x50))
       problem:
        
       Qed
 
 
 1:++(++(x,y),z) -> ++(x,++(y,z))
   ++(x,++(y,z)) -> ++(++(x,y),z)
   ++(0(),x) -> x
   Open