Problem:
 F(x,y) -> c(A())
 G(x) -> x
 h(x) -> c(x)

Proof:
 sorted: (order)
 0:F(x,y) -> c(A())
 1:G(x) -> x
 2:h(x) -> c(x)
 -----
 sorts
   [0>3, 0>8, 0>9, 1>7, 2>3, 3>4, 4>5, 4>6]
 sort attachment (non-strict)
   F : 8 x 9 -> 0
   c : 4 -> 3
   A : 5
   G : 7 -> 1
   h : 6 -> 2
 -----
 0:F(x,y) -> c(A())
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 1:G(x) -> x
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 2:h(x) -> c(x)
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed