Certification Problem

Input (COPS 1156)

We consider the TRS containing the following rules:

a(b(x))	→	b(c(x))	(1)
a(c(x))	→	c(a(x))	(2)
b(b(x))	→	a(c(x))	(3)
c(b(x))	→	b(c(x))	(4)
c(b(x))	→	c(c(x))	(5)
c(c(x))	→	c(b(x))	(6)
0(1(2(x)))	→	2(0(1(x)))	(7)
2(2(2(2(2(2(2(1(1(1(1(2(x))))))))))))	→	2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))	(8)

The underlying signature is as follows:

{a/1, b/1, c/1, 0/1, 1/1, 2/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2023)

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.

a	:	1 → 1
b	:	1 → 1
c	:	1 → 1
0	:	0 → 0
1	:	0 → 0
2	:	0 → 0

The subsystem is

(1.1)

0(1(2(x)))	→	2(0(1(x)))	(7)
2(2(2(2(2(2(2(1(1(1(1(2(x))))))))))))	→	2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))	(8)

1.1 Non-Joinable Fork

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

t₀	=	0(1(2(2(2(2(2(2(2(1(1(1(1(2(x270))))))))))))))
	→	0(1(2(1(2(2(0(1(2(1(1(0(1(0(x270))))))))))))))
	→	0(1(2(1(2(2(2(0(1(1(1(0(1(0(x270))))))))))))))
	→	2(0(1(1(2(2(2(0(1(1(1(0(1(0(x270))))))))))))))
	=	t₃

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