Certification Problem

Input (COPS 312)

The rewrite relation of the following conditional TRS is considered.

gcd(z,y) gcd(x,y) | iadd(z) ≈ tp2(x,y)
gcd(y,z) gcd(x,y) | iadd(z) ≈ tp2(x,y)
gcd(x,0) x
gcd(0,x) x
iadd(y) tp2(0,y)
iadd(s(z)) u1(iadd(z))
u1(tp2(x,y)) tp2(s(x),y)
iadd(add(x,y)) tp2(x,y)

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ConCon @ CoCo 2020)

1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.
iadd(add(z,x')) * tp2(z,x')
iadd(add(z,x')) * tp2(0,add(z,x'))
The two resulting terms cannot be joined for the following reason: