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

Proof:
 sorted: (order-sorted)
 0:b() -> c()
 1:a() -> a()
 -----
 sorts
   [0>1]
 sort attachment (non-strict)
   b : 0
   c : 1
   a : 2
 -----
 0:b() -> c()
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed
 
 
 1:a() -> a()
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed