Certification Problem

Input (COPS 47)

We consider the TRS containing the following rules:

F(x,x) → A (1)
G(x) → F(x,G(x)) (2)
C → G(C) (3)

The underlying signature is as follows:

{F/2, A/0, G/1, C/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2020)

1 Redundant Rules Transformation

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

F(x,x) → A (1)
G(x) → F(x,G(x)) (2)
C → G(C) (3)
G(C) → F(G(C),G(C)) (4)
G(C) → F(C,G(G(C))) (5)
C → F(C,G(C)) (6)
C → G(G(C)) (7)
F(F(x,x),A) → A (8)
F(A,F(x,x)) → A (9)
F(C,G(C)) → A (10)
F(G(C),C) → A (11)

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

1.1 Redundant Rules Transformation

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

F(x,x) → A (1)
G(x) → F(x,G(x)) (2)
C → G(C) (3)
G(C) → F(G(C),G(C)) (4)
G(C) → F(C,G(G(C))) (5)
C → F(C,G(C)) (6)
C → G(G(C)) (7)
F(F(x,x),A) → A (8)
F(A,F(x,x)) → A (9)
F(C,G(C)) → A (10)
F(G(C),C) → A (11)
G(C) → A (12)
C → F(G(C),G(C)) (13)
C → F(C,G(G(C))) (14)
C → G(F(C,G(C))) (15)
C → G(G(G(C))) (16)
C → F(C,F(C,G(C))) (17)
C → F(G(G(C)),G(C)) (18)
C → F(C,G(G(G(C)))) (19)
C → A (20)
C → F(G(C),G(G(C))) (21)
C → G(F(G(C),G(C))) (22)
C → G(F(C,G(G(C)))) (23)
C → G(G(F(C,G(C)))) (24)
C → G(G(G(G(C)))) (25)
F(C,F(C,G(C))) → A (26)
F(F(C,G(C)),C) → A (27)
F(C,G(G(C))) → A (28)
F(G(G(C)),C) → A (29)
F(F(C,G(C)),A) → A (30)
F(A,F(C,G(C))) → A (31)
F(F(G(C),C),A) → A (32)
F(A,F(G(C),C)) → A (33)
F(G(C),A) → A (34)
F(A,G(C)) → A (35)
F(C,C) → A (36)

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 = G(C)
→ G(A)
= t1

t0 = G(C)
→ A
= t1

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