0.00/0.51 NO 0.00/0.51 0.00/0.51 Problem: 0.00/0.51 f(x) -> y <= a() = h(y) 0.00/0.51 g(x, b()) -> g(f(c()), x) <= f(b()) = x, x = c() 0.00/0.51 a() -> h(b()) 0.00/0.51 a() -> h(c()) 0.00/0.51 0.00/0.51 Proof: 0.00/0.51 This system is not confluent. 0.00/0.51 This system is oriented. 0.00/0.51 For the unconditional CP h(b()) = h(c()) the left- and right-hand sides are two different normal forms wrt R_u. 0.00/0.51 0.00/0.53 EOF