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

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