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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  +(+(x,y),z) -> +(x,+(y,z))
  +(x,+(y,z)) -> +(+(x,y),z)
  
   T' = (P union S) with
  
   TRS P:+(+(x,y),z) -> +(x,+(y,z))
         +(x,+(y,z)) -> +(+(x,y),z)
  
   TRS S:
  
  S is left-linear and P is reversible.
  
   CP(S,S) = 
  
   CP(S,P union P^-1) = 
  
  
   PCP_in(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Qed