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

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