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

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   g(x) -> h(g(x))
   f(x) -> h(f(x))
   f(x) -> g(x)
  weak:
   
  critical peaks: 2
   h(f(x)) <-1|[]- f(x) -2|[]-> g(x)
   g(x) <-2|[]- f(x) -1|[]-> h(f(x))
  Closedness Processor (*development*):
   
   Qed