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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  f(s(x20)) -> h(s(x20),s(x20))
  g(x21) -> s(x21)
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [f](x0) = 5x0 + 4,
    
    [s](x0) = 2x0 + 2,
    
    [g](x0) = 4x0 + 4,
    
    [h](x0, x1) = 4x0 + x1 + 4
   orientation:
    f(s(x20)) = 10x20 + 14 >= 10x20 + 14 = h(s(x20),s(x20))
    
    g(x21) = 4x21 + 4 >= 2x21 + 2 = s(x21)
   problem:
    f(s(x20)) -> h(s(x20),s(x20))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [f](x0) = 2x0 + 5,
     
     [s](x0) = x0,
     
     [h](x0, x1) = x0 + x1
    orientation:
     f(s(x20)) = 2x20 + 5 >= 2x20 = h(s(x20),s(x20))
    problem:
     
    Qed