Certification Problem

Input (COPS 952)

We consider the TRS containing the following rules:

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

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(1(2(1(x))))
	→	1(2(1(1(0(1(2(0(1(2(x))))))))))
	=	t₁

t₀	=	0(1(2(1(x))))
	→	1(2(1(1(0(1(2(0(1(2(0(1(2(x)))))))))))))
	=	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.