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

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