NO Non-Confluence Proof

Non-Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

plus(x,0) x
plus(0,1) 1
plus(x,plus(y,1)) plus(plus(x,y),1)
times(x,0) 0
times(x,1) x
times(x,plus(y,1)) plus(times(x,y),x)
m(0) 0
plus(m(1),1) 0
plus(m(plus(x,1)),1) m(x)
m(m(x)) x
plus(x,m(y)) m(plus(m(x),y))
times(x,m(y)) m(times(x,y))

Proof

1 Non-Joinable Fork

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

t0 = times(c_1,plus(0,1))
ε plus(times(c_1,0),c_1)
1 plus(0,c_1)
= t2

t0 = times(c_1,plus(0,1))
2 times(c_1,1)
ε c_1
= t2

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

Tool configuration

ACP