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 2020)

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(F(E(x8),x8)),F(E(x8),x8))
→ F(E(G(x8)),F(E(x8),x8))
→ F(G(x8),F(E(x8),x8))
→ F(G(x8),F(x8,x8))
= t3

t0 = F(E(F(E(x8),x8)),F(E(x8),x8))
→ G(F(E(x8),x8))
→ G(F(x8,x8))
= t2

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