Certification Problem

Input (COPS 64)

We consider the TRS containing the following rules:

h(f,a,a)	→	h(g,a,a)	(1)
h(g,a,a)	→	h(f,a,a)	(2)
a	→	a'	(3)
h(x,a',y)	→	h(x,y,y)	(4)
h(x,y,a')	→	h(x,y,y)	(5)

The underlying signature is as follows:

{h/3, f/0, a/0, g/0, a'/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.

t₀	=	h(g,a,a)
	→	h(g,a,a')
	→	h(g,a',a')
	=	t₂

t₀	=	h(g,a,a)
	→	h(f,a,a)
	→	h(f,a,a')
	→	h(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:
    
    {33}
  - transitions:
    
    a' → 34
    
    a' → 35
    
    g → 36
    
    h(36,34,34) → 33
    
    h(36,35,35) → 33
    
    h(36,35,34) → 33
  The automaton is closed under rewriting as it is compatible.
- Automaton 2
  - final states:
    
    {29}
  - transitions:
    
    a' → 30
    
    a' → 31
    
    h(32,30,30) → 29
    
    h(32,31,31) → 29
    
    h(32,31,30) → 29
    
    f → 32
  The automaton is closed under rewriting as it is compatible.