NO Problem: a() -> h(a()) a() -> f(c()) f(x) -> h(g(x)) h(x) -> h(g(x)) Proof: Nonconfluence Processor: terms: h(f(c())) *<- a() ->* h(g(c())) Qed first automaton: final states: {8} transitions: h(10) -> 8* h(53) -> 10* c() -> 9* f(9) -> 10* g(10) -> 10* g(9) -> 53* g(53) -> 53* second automaton: final states: {14} transitions: h(16) -> 14* c() -> 15* g(15) -> 16* g(16) -> 16*