Certification Problem

Input (COPS 98)

We consider the TRS containing the following rules:

I(x) I(B(x)) (1)
F(E(x),x) G(x) (2)
E(x) x (3)

The underlying signature is as follows:

{I/1, B/1, F/2, E/1, G/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.
I : 3 → 0
B : 3 → 3
F : 2 ⨯ 2 → 1
E : 2 → 2
G : 2 → 1
The subsystem is

(1.1)

F(E(x),x) G(x) (2)
E(x) x (3)

1.1 Non-Joinable Fork

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

t0 = F(E(x),x)
F(x,x)
= t1

t0 = F(E(x),x)
G(x)
= t1

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