Problem:
 f(g(x),x) -> f(a(),x)
 f(h(x),y) -> f(h(x),h(x))
 g(x) -> p(x)
 p(x) -> a()

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   
  weak:
   
  critical peaks: 1
   f(p(x),x) <-1|0[]- f(g(x),x) -3|[]-> f(a(),x)
  Redundant Rules Transformation:
   p(x) -> a()
   g(x) -> p(x)
   g(x) -> a()
   f(h(x),y) -> f(h(x),h(x))
   f(g(x),x) -> f(a(),x)
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     
    weak:
     
    critical peaks: 2
     a() <-1|[]- g(x) -2|[]-> p(x)
     p(x) <-2|[]- g(x) -1|[]-> a()
    Redundant Rules Transformation:
     f(h(x),y) -> f(h(x),h(x))
     g(x) -> a()
     g(x) -> p(x)
     p(x) -> a()
     Church Rosser Transformation Processor (no redundant rules):
      strict:
       p(x) -> a()
       g(x) -> p(x)
       g(x) -> a()
       f(h(x),y) -> f(h(x),h(x))
      weak:
       
      critical peaks: 2
       p(x) <-1|[]- g(x) -2|[]-> a()
       a() <-2|[]- g(x) -1|[]-> p(x)
      Closedness Processor (*parallel*):
       
       Qed