NO Non-Confluence Proof

Non-Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

5(5(x)) 0(5(4(0(2(5(4(5(2(1(x))))))))))
5(5(x)) 3(4(1(1(1(1(4(4(0(4(x))))))))))
2(5(5(x))) 4(2(5(4(4(0(0(1(1(2(x))))))))))
5(2(4(x))) 0(5(0(2(3(3(4(2(4(2(x))))))))))
5(5(2(x))) 0(1(3(2(3(0(3(2(5(3(x))))))))))
5(5(3(x))) 0(3(5(4(4(1(0(1(5(0(x))))))))))
5(5(5(x))) 5(3(4(1(0(1(4(5(0(0(x))))))))))
2(5(0(4(x)))) 4(4(3(2(4(4(5(1(0(0(x))))))))))
4(5(2(4(x)))) 4(1(5(5(2(0(3(1(3(3(x))))))))))
4(5(5(5(x)))) 1(5(1(2(0(3(2(1(0(5(x))))))))))
0(2(5(3(4(x))))) 3(2(4(3(1(5(1(1(3(4(x))))))))))
2(5(5(3(4(x))))) 4(5(4(3(1(4(0(2(4(4(x))))))))))
5(5(5(1(4(x))))) 3(3(0(5(0(4(3(4(4(0(x))))))))))
0(4(4(5(5(5(x)))))) 0(4(4(4(3(3(4(1(3(1(x))))))))))
1(2(4(5(2(4(x)))))) 3(3(5(3(0(4(0(3(1(3(x))))))))))
4(1(5(5(0(4(x)))))) 1(0(3(0(4(2(4(4(3(4(x))))))))))
4(2(5(5(1(5(x)))))) 2(3(4(2(1(1(3(4(2(5(x))))))))))
5(2(5(5(0(4(x)))))) 0(4(2(3(3(5(2(1(4(4(x))))))))))
5(5(2(4(5(0(x)))))) 2(1(1(4(2(4(0(4(2(0(x))))))))))
0(1(5(5(5(3(5(x))))))) 5(3(2(5(1(0(1(2(0(5(x))))))))))
4(4(5(2(4(2(2(x))))))) 4(0(5(5(4(5(1(2(2(1(x))))))))))

Proof

1 Non-Joinable Fork

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

t0 = 5(5(c_1))
ε 0(5(4(0(2(5(4(5(2(1(c_1))))))))))
= t1

t0 = 5(5(c_1))
ε 3(4(1(1(1(1(4(4(0(4(c_1))))))))))
= t1

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

Tool configuration

ACP