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

Proof:
 sorted: (order-sorted)
 0:h(b(),a()) -> a()
   a() -> c()
   h(c(),c()) -> a()
 1:f(b()) -> c()
 -----
 sorts
   [0>2, 0>3, 1>5, 1>6, 2>5, 2>7, 3>4, 4>5, 6>7]
 sort attachment (non-strict)
   h : 2 x 3 -> 0
   b : 7
   a : 4
   c : 5
   f : 6 -> 1
 -----
 0:h(b(),a()) -> a()
   a() -> c()
   h(c(),c()) -> a()
   Nonconfluence Processor:
    terms: h(b(),c()) *<- h(b(),a()) ->* a()
    Qed
    
    first automaton:
     final states: {1}
     transitions:
      c() -> 2*
      b() -> 3*
      h(3,2) -> 1*
    
    second automaton:
     final states: {4}
     transitions:
      c() -> 4*
      a() -> 4*
 
 
 1:f(b()) -> c()
   Open