Problem:
 f(b()) -> c()
 c() -> c()
 f(c()) -> b()
 a() -> b()

Proof:
 sorted: (order-sorted)
 0:f(b()) -> c()
   c() -> c()
   f(c()) -> b()
 1:a() -> b()
 -----
 sorts
   [0>2, 1>4, 2>3, 2>4]
 sort attachment (non-strict)
   f : 2 -> 0
   b : 4
   c : 3
   a : 1
 -----
 0:f(b()) -> c()
   c() -> c()
   f(c()) -> b()
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.4):
    f(c()) -> b()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [f](x0) = x0 + 1,
      
      [b] = 0,
      
      [c] = 4
     orientation:
      f(c()) = 5 >= 0 = b()
     problem:
      
     Qed
 
 
 1:a() -> b()
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed