0.00/0.66 NO 0.00/0.66 0.00/0.66 Problem: 0.00/0.66 gcd(z, y) -> gcd(x, y) <= iadd(z) = tp2(x, y) 0.00/0.66 gcd(y, z) -> gcd(x, y) <= iadd(z) = tp2(x, y) 0.00/0.66 gcd(x, 0()) -> x 0.00/0.66 gcd(0(), x) -> x 0.00/0.66 iadd(y) -> tp2(0(), y) 0.00/0.66 iadd(s(z)) -> u1(iadd(z)) 0.00/0.66 u1(tp2(x, y)) -> tp2(s(x), y) 0.00/0.66 iadd(add(x, y)) -> tp2(x, y) 0.00/0.66 0.00/0.66 Proof: 0.00/0.66 This system is not confluent. 0.00/0.66 This system is oriented. 0.00/0.66 For the unconditional CP tp2(x, y) = tp2(0(), add(x, y)) the left- and right-hand sides are two different normal forms wrt R_u. 0.00/0.66 0.00/0.68 EOF