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 (ac):
    F(x,A(G(x))) -> G(F(x,x))
    F(x,G(x)) -> G(F(x,x))
    A(x) -> x
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      A > F > G
      weight function:
       w0 = 1
       w(G) = 2
       w(F) = w(A) = 0
      problem:
       
      Qed