Certification Problem

Input (COPS 972)

We consider the TRS containing the following rules:

0(x)	→	1(x)	(1)
0(0(x))	→	0(x)	(2)
3(4(5(x)))	→	4(3(5(x)))	(3)
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(4)
0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(5)

The underlying signature is as follows:

{0/1, 1/1, 3/1, 4/1, 5/1, 2/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2022)

1 Persistent Decomposition (Many-Sorted)

Non-confluence is proven, because a system induced by the sorts in the following many-sorted sort attachment is not confluent.

0	:	2 → 2
1	:	2 → 2
3	:	0 → 0
4	:	0 → 0
5	:	1 → 0
2	:	2 → 2

The subsystem is

(1.1)

0(x)	→	1(x)	(1)
0(0(x))	→	0(x)	(2)
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(4)
0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(5)

1.1 Non-Joinable Fork

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

t₀	=	2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))
	→	2(1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))
	=	t₁

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