Problem:
 F(x,A(G(x))) -> G(F(x,x))
 F(x,G(x)) -> G(F(x,x))
 A(x) -> x
 H(x) -> H(B(H(x)))

Proof:
 sorted: (order)
 0:H(x) -> H(B(H(x)))
 1:F(x,A(G(x))) -> G(F(x,x))
   F(x,G(x)) -> G(F(x,x))
   A(x) -> x
 -----
 sorts
   []
 sort attachment (non-strict)
   F : 1 x 1 -> 1
   A : 1 -> 1
   G : 1 -> 1
   H : 0 -> 0
   B : 0 -> 0
 -----
 0:H(x) -> H(B(H(x)))
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 1:F(x,A(G(x))) -> G(F(x,x))
   F(x,G(x)) -> G(F(x,x))
   A(x) -> x
   Church Rosser Transformation Processor:
    strict:
     
    weak:
     
    critical peaks: 1
     F(x,G(x)) <-2|1[]- F(x,A(G(x))) -0|[]-> G(F(x,x))
    Redundant Rules Transformation:
     F(x,G(x)) -> G(F(x,x))
     A(x) -> x
     Church Rosser Transformation Processor (kb):
      F(x,G(x)) -> G(F(x,x))
      A(x) -> x
      critical peaks: joinable
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [F](x0, x1) = x0 + x1 + 4,
        
        [A](x0) = x0 + 1,
        
        [G](x0) = x0 + 2
       orientation:
        F(x,G(x)) = 2x + 6 >= 2x + 6 = G(F(x,x))
        
        A(x) = x + 1 >= x = x
       problem:
        F(x,G(x)) -> G(F(x,x))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [F](x0, x1) = x0 + 2x1 + 4,
         
         [G](x0) = x0 + 1
        orientation:
         F(x,G(x)) = 3x + 6 >= 3x + 5 = G(F(x,x))
        problem:
         
        Qed