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

Proof:
 sorted: (order)
 0:f(x,y) -> x
   f(x,y) -> f(x,g(y))
   g(x) -> h(x)
 1:g(x) -> h(x)
   F(g(x),x) -> F(x,g(x))
   F(h(x),x) -> F(x,h(x))
 -----
 sorts
   [1>4, 1>5, 2>3, 3>5]
 sort attachment (non-strict)
   f : 4 x 5 -> 1
   g : 5 -> 5
   h : 5 -> 5
   F : 3 x 5 -> 2
 -----
 0:f(x,y) -> x
   f(x,y) -> f(x,g(y))
   g(x) -> h(x)
   Church Rosser Transformation Processor:
    
    strict:
     
    weak:
     
    critical peaks: 2
    x <-0|[]- f(x,y) -1|[]-> f(x,g(y))
    f(x,g(y)) <-1|[]- f(x,y) -0|[]-> x
    Closedness Processor (*parallel*):
     
     strict:
      
     weak:
      
     Qed
 
 
 1:g(x) -> h(x)
   F(g(x),x) -> F(x,g(x))
   F(h(x),x) -> F(x,h(x))
   Church Rosser Transformation Processor (kb):
    g(x) -> h(x)
    F(g(x),x) -> F(x,g(x))
    F(h(x),x) -> F(x,h(x))
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [F](x0, x1) = 5x0 + 4x1,
      
      [h](x0) = 3x0,
      
      [g](x0) = 4x0 + 4
     orientation:
      g(x) = 4x + 4 >= 3x = h(x)
      
      F(g(x),x) = 24x + 20 >= 21x + 16 = F(x,g(x))
      
      F(h(x),x) = 19x >= 17x = F(x,h(x))
     problem:
      F(h(x),x) -> F(x,h(x))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [F](x0, x1) = 4x0 + 3x1 + 3,
       
       [h](x0) = 4x0 + 7
      orientation:
       F(h(x),x) = 19x + 31 >= 16x + 24 = F(x,h(x))
      problem:
       
      Qed