Problem:
 F(x,y) -> c(y)
 G(x) -> x
 f(x) -> g(x)
 g(x) -> c(x)

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