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