Certification Problem

Input (COPS 569)

We consider the TRS containing the following rules:

s(p(x))	→	x	(1)
p(s(x))	→	x	(2)
+(x,0)	→	x	(3)
+(x,s(y))	→	s(+(x,y))	(4)
+(x,p(y))	→	p(+(x,y))	(5)
-(x,0)	→	x	(6)
-(x,s(y))	→	p(-(x,y))	(7)
-(x,p(y))	→	s(-(x,y))	(8)
*(x,0)	→	0	(9)
*(x,s(y))	→	+(*(x,y),x)	(10)
*(x,p(y))	→	-(*(x,y),x)	(11)

The underlying signature is as follows:

{s/1, p/1, +/2, 0/0, -/2, */2}

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₀	=	*(f7,s(p(f10)))
	→	*(f7,f10)
	=	t₁

t₀	=	*(f7,s(p(f10)))
	→	+(*(f7,p(f10)),f7)
	=	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:
    
    {28}
  - transitions:
    
    f7 → 30
    
    *(30,29) → 28
    
    f10 → 29
  The automaton is closed under rewriting as it is compatible.
- Automaton 2
  - final states:
    
    {31}
  - transitions:
    
    f7 → 32
    
    f7 → 35
    
    *(35,34) → 36
    
    *(35,33) → 95
    
    f10 → 33
    
    -(95,35) → 36
    
    p(33) → 34
    
    +(36,32) → 31
  The automaton is closed under rewriting as it is compatible.