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