Certification Problem

Input (COPS 541)

We consider the TRS containing the following rules:

+(a,b)	→	b	(1)
+(c,a)	→	a	(2)
+(x,y)	→	+(y,x)	(3)
+(+(x,y),z)	→	+(x,+(y,z))	(4)

The underlying signature is as follows:

{+/2, a/0, b/0, c/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2021)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

+(a,b)	→	b	(1)
+(c,a)	→	a	(2)
+(x,y)	→	+(y,x)	(3)
+(+(x,y),z)	→	+(x,+(y,z))	(4)
+(b,a)	→	b	(5)
+(a,c)	→	a	(6)
+(y,x)	→	+(y,x)	(7)
+(a,+(a,b))	→	b	(8)
+(+(c,a),b)	→	b	(9)
+(c,+(c,a))	→	a	(10)
+(x,y)	→	+(x,y)	(11)

All redundant rules that were added or removed can be simulated in 3 steps .

1.1 Non-Joinable Fork

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

t₀	=	+(+(c,a),b)
	→	+(c,+(a,b))
	→	+(c,b)
	=	t₂

t₀	=	+(+(c,a),b)
	→	b
	=	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:
    
    {198}
  - transitions:
    
    +(200,199) → 198
    
    +(199,200) → 198
    
    b → 199
    
    c → 200
  The automaton is closed under rewriting as it is compatible.
- Automaton 2
  - final states:
    
    {25}
  - transitions:
    
    b → 25
  The automaton is closed under rewriting as it is compatible.