Problem:
 f(a()) -> f(g(b(),b()))
 a() -> g(c(),c())
 c() -> d()
 d() -> b()
 b() -> d()

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