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