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

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