NO Problem: c() -> f(b()) c() -> b() Proof: Nonconfluence Processor: terms: b() *<- c() ->* f(b()) Qed first automaton: final states: {1} transitions: b() -> 1* second automaton: final states: {2} transitions: b() -> 3* f(3) -> 2*