Certification Problem

Input (COPS 968)

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...))))))))))))))))))))))))))))))))))))))))))))))))))) 0(0(1(1(1(1(0(0(1(0(0(1(0(1(1(1(0(0(1(0(1(1(0(0(0(0(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (4)
1(1(1(1(1(0(1(0(1(1(1(1(1(0(1(1(0(1(1(1(0(0(0(0(0(0(0(0(1(1(0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(0(1(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 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.
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...))))))))))))))))))))))))))))))))))))))))))))))))))) 0(0(1(1(1(1(0(0(1(0(0(1(0(1(1(1(0(0(1(0(1(1(0(0(0(0(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (4)
1(1(1(1(1(0(1(0(1(1(1(1(1(0(1(1(0(1(1(1(0(0(0(0(0(0(0(0(1(1(0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(0(1(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 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

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...))))))))))))))))))))))))))))))))))))))))))))))))))) 0(0(1(1(1(1(0(0(1(0(0(1(0(1(1(1(0(0(1(0(1(1(0(0(0(0(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (4)
1(1(1(1(1(0(1(0(1(1(1(1(1(0(1(1(0(1(1(1(0(0(0(0(0(0(0(0(1(1(0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(0(1(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)
0(0(x)) 1(1(x)) (6)
0(0(0(x))) 1(0(x)) (7)
0(0(x)) 1(x) (8)
0(0(0(x))) 0(1(x)) (9)
0(0(0(x))) 0(x) (10)
0(0(0(x2796))) 0(x2796) (11)

All redundant rules that were added or removed can be simulated in 3 steps .

1.1.1 Non-Joinable Fork

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

t0 = 0(0(x))
1(1(x))
= t1

t0 = 0(0(x))
1(x)
= t1

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