NO Problem: c() -> f(c()) c() -> f(h(a())) f(x) -> h(f(x)) Proof: Nonconfluence Processor: terms: f(h(a())) *<- c() ->* f(f(h(a()))) Qed first automaton: final states: {1} transitions: f(3) -> 1* a() -> 2* h(2) -> 3* h(1) -> 1* second automaton: final states: {9} transitions: f(12) -> 9* f(11) -> 12* a() -> 10* h(10) -> 11* h(12) -> 12* h(9) -> 9*