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

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