Certification Problem

Input (COPS 741)

We consider the TRS containing the following rules:

if(true,a,x)	→	a	(1)
if(true,b,x)	→	b	(2)
if(true,g(a),x)	→	g(a)	(3)
if(true,g(b),x)	→	g(b)	(4)
if(false,x,a)	→	a	(5)
if(false,x,b)	→	b	(6)
if(false,x,g(a))	→	g(a)	(7)
if(false,x,g(b))	→	g(b)	(8)
g(a)	→	g(g(a))	(9)
g(b)	→	a	(10)
f(a,b)	→	b	(11)
f(g(g(a)),x)	→	b	(12)

The underlying signature is as follows:

{if/3, true/0, a/0, b/0, g/1, false/0, f/2}

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₀	=	if(true,g(a),f7)
	→	if(true,g(g(a)),f7)
	=	t₁

t₀	=	if(true,g(a),f7)
	→	g(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:
    
    {26}
  - transitions:
    
    f7 → 27
    
    g(28) → 29
    
    g(29) → 30
    
    g(29) → 29
    
    if(31,30,27) → 26
    
    a → 28
    
    true → 31
  The automaton is closed under rewriting as it is compatible.
- Automaton 2
  - final states:
    
    {24}
  - transitions:
    
    g(24) → 24
    
    g(25) → 24
    
    a → 25
  The automaton is closed under rewriting as it is compatible.