Problem:
 f(x) -> g(x)
 a(x,y) -> a(f(x),f(x))
 b(x,y) -> c(x,x)
 c(x,x) -> c(f(x),f(x))

Proof:
 sorted: (order)
 0:f(x) -> g(x)
   a(x,y) -> a(f(x),f(x))
 1:f(x) -> g(x)
   b(x,y) -> c(x,x)
   c(x,x) -> c(f(x),f(x))
 -----
 sorts
   [1>5, 2>3, 2>4, 3>6, 5>6]
 sort attachment (strict)
   f : 6 -> 6
   g : 6 -> 6
   a : 6 x 5 -> 1
   b : 6 x 4 -> 2
   c : 6 x 6 -> 3
 -----
 0:f(x) -> g(x)
   a(x,y) -> a(f(x),f(x))
   Church Rosser Transformation Processor:
    
    strict:
     
    weak:
     
    critical peaks: 0
    Qed
 
 
 1:f(x) -> g(x)
   b(x,y) -> c(x,x)
   c(x,x) -> c(f(x),f(x))
   Open