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
   [0>3, 0>4, 1>2, 2>4]
 sort attachment (non-strict)
   f : 3 x 4 -> 0
   g : 4 -> 4
   h : 4 -> 4
   F : 2 x 4 -> 1
 -----
 0:f(x,y) -> x
   f(x,y) -> f(x,g(y))
   g(x) -> h(x)
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    f(x23,x22) -> x23
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [f](x0, x1) = 4x0 + 2x1 + 4
     orientation:
      f(x23,x22) = 2x22 + 4x23 + 4 >= x23 = x23
     problem:
      
     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 (ac):
    g(x) -> h(x)
    F(g(x),x) -> F(x,g(x))
    F(h(x),x) -> F(x,h(x))
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      F > g > h
      weight function:
       w0 = 1
       w(h) = w(g) = 2
       w(F) = 0
      problem:
       
      Qed