Certification Problem

Input (COPS 980)

We consider the TRS containing the following rules:

a(x)	→	b(x)	(1)
b(b(c(x)))	→	c(a(c(a(a(x)))))	(2)
c(c(x))	→	x	(3)

The underlying signature is as follows:

{a/1, b/1, c/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₀	=	b(b(c(c(f3))))
	→	b(b(f3))
	=	t₁

t₀	=	b(b(c(c(f3))))
	→	c(a(c(a(a(c(f3))))))
	=	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:
  
  {3}
- transitions:
  
  b(5) → 3
  
  b(4) → 5
  
  f3 → 4
The automaton is closed under rewriting as it is compatible.

Automaton 2

final states:

{6}

transitions:

49	→	11
151	→	6
c(10)	→	11
c(47)	→	48
c(149)	→	150
c(49)	→	10
c(151)	→	12
c(12)	→	6
c(7)	→	8
b(48)	→	49
b(47)	→	148
b(148)	→	149
b(150)	→	151
b(11)	→	12
b(7)	→	46
b(9)	→	10
b(8)	→	9
b(46)	→	47
a(48)	→	49
a(148)	→	149
a(11)	→	12
a(9)	→	10
a(46)	→	47
a(150)	→	151
a(8)	→	9
a(7)	→	46
a(47)	→	148
f3	→	7

The automaton is closed under rewriting as it is compatible.