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