NO Problem: h(b(),a()) -> a() a() -> c() h(c(),c()) -> a() f(b()) -> c() Proof: sorted: (order-sorted) 0:h(b(),a()) -> a() a() -> c() h(c(),c()) -> a() 1:f(b()) -> c() ----- sorts [0>2, 0>3, 1>5, 1>6, 2>5, 2>7, 3>4, 4>5, 6>7] sort attachment (non-strict) h : 2 x 3 -> 0 b : 7 a : 4 c : 5 f : 6 -> 1 ----- 0:h(b(),a()) -> a() a() -> c() h(c(),c()) -> a() Nonconfluence Processor: terms: h(b(),c()) *<- h(b(),a()) ->* a() Qed first automaton: final states: {1} transitions: c() -> 2* b() -> 3* h(3,2) -> 1* second automaton: final states: {4} transitions: c() -> 4* a() -> 4* 1:f(b()) -> c() Open