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