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()) ->* c() Qed 1:f(b()) -> c() Open