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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.4):
  f(f(a())) -> c()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [f](x0) = x0 + 5,
    
    [c] = 0,
    
    [a] = 5
   orientation:
    f(f(a())) = 15 >= 0 = c()
   problem:
    
   Qed