YES

Problem:
 a() -> b()
 b() -> a()
 a() -> d()

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  b() -> a()
  a() -> d()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [b] = 4,
    
    [a] = 4,
    
    [d] = 0
   orientation:
    b() = 4 >= 4 = a()
    
    a() = 4 >= 0 = d()
   problem:
    b() -> a()
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b] = 1,
     
     [a] = 0
    orientation:
     b() = 1 >= 0 = a()
    problem:
     
    Qed