Problem:
 a() -> b()
 f(a()) -> g(a())
 f(b()) -> g(b())

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  f(b()) -> g(b())
  a() -> b()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [g](x0) = 2x0,
    
    [f](x0) = x0 + 4,
    
    [b] = 4,
    
    [a] = 5
   orientation:
    f(b()) = 8 >= 8 = g(b())
    
    a() = 5 >= 4 = b()
   problem:
    f(b()) -> g(b())
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [g](x0) = x0,
     
     [f](x0) = x0 + 1,
     
     [b] = 6
    orientation:
     f(b()) = 7 >= 6 = g(b())
    problem:
     
    Qed