Problem:
 f(x) -> g(k(x))
 f(x) -> a()
 g(x) -> a()
 k(a()) -> k(k(a()))

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