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

Proof:
 sorted: (order-sorted)
 0:f(a()) -> c()
 1:b() -> c()
   b() -> a()
 -----
 sorts
   [0>2, 0>3, 1>2, 1>4, 3>4]
 sort attachment (non-strict)
   f : 3 -> 0
   a : 4
   c : 2
   b : 1
 -----
 0:f(a()) -> c()
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed
 
 
 1:b() -> c()
   b() -> a()
   Nonconfluence Processor:
    terms: a() *<- b() ->* c()
    Qed
    
    first automaton:
     final states: {1}
     transitions:
      a() -> 1*
    
    second automaton:
     final states: {2}
     transitions:
      c() -> 2*