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

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