Certification Problem

Input (COPS 574)

We consider the TRS containing the following rules:

+(0,y)	→	y	(1)
+(s(0),y)	→	s(y)	(2)
+(+(x,y),z)	→	+(x,+(y,z))	(3)
+(x,y)	→	+(y,x)	(4)
s(s(x))	→	s(x)	(5)
s(x)	→	s(s(x))	(6)

The underlying signature is as follows:

{+/2, 0/0, s/1}

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₀	=	+(+(s(0),f99),f98)
	→	+(s(f99),f98)
	=	t₁

t₀	=	+(+(s(0),f99),f98)
	→	+(s(0),+(f99,f98))
	→	s(+(f99,f98))
	=	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:
    
    {214}
  - transitions:
    
    f98 → 215
    
    s(216) → 217
    
    s(217) → 217
    
    +(217,215) → 214
    
    +(215,217) → 214
    
    f99 → 216
  The automaton is closed under rewriting as it is compatible.
- Automaton 2
  - final states:
    
    {224}
  - transitions:
    
    f98 → 225
    
    s(224) → 224
    
    s(227) → 224
    
    +(225,226) → 227
    
    +(226,225) → 227
    
    f99 → 226
  The automaton is closed under rewriting as it is compatible.