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: