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