NO Non-Confluence Proof

Non-Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

+(0,y) → y
+(s(x),y) → s(+(x,y))
+(x,0) → +(0,x)
+(x,s(y)) → +(s(y),x)

Proof

1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.

t0 = +(s(x306),s(y))
→ε s(+(x306,s(y)))
→1 s(+(s(y),x306))
→1 s(s(+(y,x306)))
= t3

t0 = +(s(x306),s(y))
→ε +(s(y),s(x306))
→ε s(+(y,s(x306)))
→1 s(+(s(x306),y))
→1 s(s(+(x306,y)))
= t4

The two resulting terms cannot be joined for the following reason:

Tool configuration

csi