Problem:
 p(x) -> q(x)
 p(x) -> r(x)
 q(x) -> s(p(x))
 r(x) -> s(p(x))
 s(x) -> f(p(x))

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   p(x) -> q(x)
   p(x) -> r(x)
   q(x) -> s(p(x))
   r(x) -> s(p(x))
   s(x) -> f(p(x))
  weak:
   
  critical peaks: 2
  q(x) <-0|[]- p(x) -1|[]-> r(x)
  r(x) <-1|[]- p(x) -0|[]-> q(x)
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed