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

Proof:
 sorted: (order-sorted)
 0:f(x,x) -> g(x)
   g(h(x)) -> h(g(x))
 1:g(h(x)) -> h(g(x))
   a(x,y) -> a(h(x),y)
 -----
 sorts
   [0>2, 1>2, 1>4, 2>3]
 sort attachment (non-strict)
   f : 3 x 3 -> 0
   g : 2 -> 2
   h : 2 -> 2
   a : 2 x 4 -> 1
 -----
 0:f(x,x) -> g(x)
   g(h(x)) -> h(g(x))
   Church Rosser Transformation Processor (kb):
    f(x,x) -> g(x)
    g(h(x)) -> h(g(x))
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [g](x0) = 4x0 + 2,
      
      [f](x0, x1) = x0 + 3x1 + 2,
      
      [h](x0) = 5x0 + 6
     orientation:
      f(x,x) = 4x + 2 >= 4x + 2 = g(x)
      
      g(h(x)) = 20x + 26 >= 20x + 16 = h(g(x))
     problem:
      f(x,x) -> g(x)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [g](x0) = 5x0,
       
       [f](x0, x1) = x0 + 4x1 + 1
      orientation:
       f(x,x) = 5x + 1 >= 5x = g(x)
      problem:
       
      Qed
 
 
 1:g(h(x)) -> h(g(x))
   a(x,y) -> a(h(x),y)
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed