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

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