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

Proof:
 sorted: (order)
 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
   [1>3, 2>3, 2>5, 3>4]
 sort attachment (non-strict)
   f : 4 x 4 -> 1
   g : 3 -> 3
   h : 3 -> 3
   a : 3 x 5 -> 2
 -----
 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:
      [h](x0) = x0 + 4,
      
      [g](x0) = 3x0 + 4,
      
      [f](x0, x1) = 5x0 + x1 + 4
     orientation:
      f(x,x) = 6x + 4 >= 3x + 4 = g(x)
      
      g(h(x)) = 3x + 16 >= 3x + 8 = h(g(x))
     problem:
      f(x,x) -> g(x)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [g](x0) = 2x0,
       
       [f](x0, x1) = x0 + x1 + 1
      orientation:
       f(x,x) = 2x + 1 >= 2x = g(x)
      problem:
       
      Qed
 
 
 1:g(h(x)) -> h(g(x))
   a(x,y) -> a(h(x),y)
   Church Rosser Transformation Processor:
    
    strict:
     
    weak:
     
    critical peaks: 0
    Qed