Problem:
 f(x) -> x
 f(x) -> f(f(x))

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