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