YES

Problem:
 a(x) -> b(x)
 a(b(x)) -> b(a(c(a(x))))
 b(x) -> c(x)
 c(c(x)) -> x

Proof:
 Church Rosser Transformation Processor:
  a(x80) -> b(x80)
  b(x83) -> c(x83)
  c(c(x85)) -> x85
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [c](x0) = 2x0 + 4,
    
    [b](x0) = 4x0 + 4,
    
    [a](x0) = 4x0 + 4
   orientation:
    a(x80) = 4x80 + 4 >= 4x80 + 4 = b(x80)
    
    b(x83) = 4x83 + 4 >= 2x83 + 4 = c(x83)
    
    c(c(x85)) = 4x85 + 12 >= x85 = x85
   problem:
    a(x80) -> b(x80)
    b(x83) -> c(x83)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [c](x0) = 4x0,
     
     [b](x0) = 4x0 + 4,
     
     [a](x0) = 4x0 + 4
    orientation:
     a(x80) = 4x80 + 4 >= 4x80 + 4 = b(x80)
     
     b(x83) = 4x83 + 4 >= 4x83 = c(x83)
    problem:
     a(x80) -> b(x80)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b](x0) = 4x0,
      
      [a](x0) = 4x0 + 1
     orientation:
      a(x80) = 4x80 + 1 >= 4x80 = b(x80)
     problem:
      
     Qed