Certification Problem

Input (COPS 49)

We consider the TRS containing the following rules:

F(A,A) G(B,B) (1)
A A' (2)
F(A',x) F(x,x) (3)
F(x,A') F(x,x) (4)
G(B,B) F(A,A) (5)
B B' (6)
G(B',x) G(x,x) (7)
G(x,B') G(x,x) (8)

The underlying signature is as follows:

{F/2, A/0, G/2, B/0, A'/0, B'/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2020)

1 Non-Joinable Fork

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

t0 = G(B,B)
G(B,B')
G(B',B')
= t2

t0 = G(B,B)
F(A,A)
F(A,A')
F(A',A')
= t3

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