Certification Problem

Input (COPS 949)

We consider the TRS containing the following rules:

0(0(0(1(2(1(1(1(0(0(1(0(1(x)))))))))))))	→	0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x)))))))))))))))))	(1)
0(0(1(0(0(1(1(1(0(1(2(0(1(x)))))))))))))	→	0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x)))))))))))))))))	(2)
0(0(1(0(1(0(1(0(0(1(0(2(0(x)))))))))))))	→	0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x)))))))))))))))))	(3)
0(0(1(1(1(1(1(2(1(1(2(1(1(x)))))))))))))	→	0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x)))))))))))))))))	(4)
0(1(0(2(0(2(1(0(0(1(0(1(1(x)))))))))))))	→	0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x)))))))))))))))))	(5)
0(1(0(2(2(1(1(2(1(2(2(0(1(x)))))))))))))	→	0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x)))))))))))))))))	(6)
0(1(1(0(1(1(0(1(0(2(1(0(0(x)))))))))))))	→	0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x)))))))))))))))))	(7)
0(1(1(1(2(1(2(0(1(2(1(0(1(x)))))))))))))	→	0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x)))))))))))))))))	(8)
0(2(0(0(1(1(2(0(1(0(1(0(2(x)))))))))))))	→	0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x)))))))))))))))))	(9)
1(0(2(0(0(2(0(1(2(0(1(0(1(x)))))))))))))	→	1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x)))))))))))))))))	(10)
1(0(2(0(2(1(0(2(0(1(1(2(0(x)))))))))))))	→	1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x)))))))))))))))))	(11)
1(1(0(0(2(2(2(0(1(2(0(1(1(x)))))))))))))	→	1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x)))))))))))))))))	(12)
1(2(0(1(0(2(0(1(0(1(2(1(0(x)))))))))))))	→	1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x)))))))))))))))))	(13)
1(2(1(2(0(0(0(1(1(1(0(0(1(x)))))))))))))	→	1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x)))))))))))))))))	(14)
2(0(0(0(2(2(0(2(2(0(1(0(1(x)))))))))))))	→	2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x)))))))))))))))))	(15)
2(0(2(1(0(0(1(0(0(0(1(1(1(x)))))))))))))	→	0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x)))))))))))))))))	(16)
2(0(2(1(1(1(1(0(2(0(1(0(1(x)))))))))))))	→	2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x)))))))))))))))))	(17)
2(1(2(2(1(1(2(2(0(1(1(0(1(x)))))))))))))	→	2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x)))))))))))))))))	(18)
2(2(1(1(1(1(0(1(1(2(0(1(0(x)))))))))))))	→	0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x)))))))))))))))))	(19)

The underlying signature is as follows:

{0/1, 1/1, 2/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2023)

1 Non-Joinable Fork

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

t₀	=	0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x4707)))))))))))))))))))))
	→	0(0(0(1(2(1(1(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x4707)))))))))))))))))))))))))
	=	t₁

t₀	=	0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x4707)))))))))))))))))))))
	→	0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(1(0(0(1(0(2(0(x4707)))))))))))))))))))))))))
	=	t₁

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

When applying the cap-function on both terms (where variables may be treated like constants) then the resulting terms do not unify.