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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   f(x) -> g(k(x))
   f(x) -> a()
   g(x) -> a()
   k(a()) -> k(k(a()))
  weak:
   
  critical peaks: 2
  g(k(x)) <-0|[]- f(x) -1|[]-> a()
  a() <-1|[]- f(x) -0|[]-> g(k(x))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed