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))
*(0,y) → 0
*(s(x),y) → +(*(x,y),y)
*(x,s(y)) → +(x,*(x,y))

Proof

1 Non-Joinable Fork

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

t0 = *(s(x182),s(y))
→ε +(*(x182,s(y)),s(y))
→1 +(+(x182,*(x182,y)),s(y))
= t2

t0 = *(s(x182),s(y))
→ε +(s(x182),*(s(x182),y))
→2 +(s(x182),+(*(x182,y),y))
→ε s(+(x182,+(*(x182,y),y)))
= t3

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

Tool configuration

csi