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