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

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: