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

Proof:
 Church Rosser Transformation Processor (ac):
  f(x,x) -> a()
  f(x,g(x)) -> b()
  AC critical peaks: joinable
  AC-KBO Processor:
   precedence:
    g > f > a > b
    weight function:
     w0 = 2
     w(b) = w(a) = 4
     w(g) = 1
     w(f) = 0
    problem:
     
    Qed