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