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