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 (critical pair closing system, Thm 2.11):
  q(x28) -> s(p(x28))
  r(x29) -> s(p(x29))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [q](x0) = x0,
    
    [s](x0) = x0,
    
    [p](x0) = x0,
    
    [r](x0) = x0 + 1
   orientation:
    q(x28) = x28 >= x28 = s(p(x28))
    
    r(x29) = x29 + 1 >= x29 = s(p(x29))
   problem:
    q(x28) -> s(p(x28))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [q](x0) = 2x0 + 1,
     
     [s](x0) = x0,
     
     [p](x0) = 2x0
    orientation:
     q(x28) = 2x28 + 1 >= 2x28 = s(p(x28))
    problem:
     
    Qed