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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 2
   g(f(x)) <-0|[]- f(x) -2|[]-> h(f(x))
   h(f(x)) <-2|[]- f(x) -0|[]-> g(f(x))
  Redundant Rules Transformation:
   h(x) -> p(h(x))
   f(x) -> h(f(x))
   g(x) -> p(p(h(x)))
   Qed (ToyamaOyamaguchi95Cor22)