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
   [0>4, 1>2, 1>3, 2>5, 4>5]
 sort attachment (strict)
   f : 5 -> 5
   g : 5 -> 5
   a : 5 x 4 -> 0
   b : 5 x 3 -> 1
   c : 5 x 5 -> 2
 -----
 0:f(x) -> g(x)
   a(x,y) -> a(f(x),f(x))
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 1:f(x) -> g(x)
   b(x,y) -> c(x,x)
   c(x,x) -> c(f(x),f(x))
   Open