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