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
   [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:
      [h](x0) = x0 + 2,
      
      [g](x0) = 2x0 + 2,
      
      [f](x0, x1) = x0 + x1 + 2
     orientation:
      f(x,x) = 2x + 2 >= 2x + 2 = g(x)
      
      g(h(x)) = 2x + 6 >= 2x + 4 = h(g(x))
     problem:
      f(x,x) -> g(x)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [g](x0) = 7x0,
       
       [f](x0, x1) = x0 + 6x1 + 1
      orientation:
       f(x,x) = 7x + 1 >= 7x = g(x)
      problem:
       
      Qed
 
 
 1:g(h(x)) -> h(g(x))
   a(x,y) -> a(h(x),y)
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed