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:
    [b] = 4,
    
    [g](x0) = 4x0,
    
    [a] = 5,
    
    [f](x0) = 3x0 + 4
   orientation:
    f(b()) = 16 >= 16 = g(b())
    
    a() = 5 >= 4 = b()
   problem:
    f(b()) -> g(b())
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b] = 2,
     
     [g](x0) = x0 + 6,
     
     [f](x0) = x0 + 7
    orientation:
     f(b()) = 9 >= 8 = g(b())
    problem:
     
    Qed