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

1 Non-Joinable Fork

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

t₀	=	G(B,B)
	→	G(B,B')
	→	G(B',B')
	=	t₂

t₀	=	G(B,B)
	→	F(A,A)
	→	F(A,A')
	→	F(A',A')
	=	t₃

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

The reachable terms of these two terms are approximated via the following two tree automata, and the tree automata have an empty intersection.
- Automaton 1
  - final states:
    
    {1}
  - transitions:
    
    B' → 2
    
    B' → 3
    
    G(3,3) → 1
    
    G(2,2) → 1
    
    G(3,2) → 1
  The automaton is closed under rewriting as it is compatible.
- Automaton 2
  - final states:
    
    {22}
  - transitions:
    
    A' → 23
    
    A' → 24
    
    F(24,24) → 22
    
    F(24,23) → 22
    
    F(23,23) → 22
  The automaton is closed under rewriting as it is compatible.