Certification Problem

Input (COPS 689)

We consider the TRS containing the following rules:

b	→	h(h(b,a),f(a))	(1)
h(h(a,c),b)	→	b	(2)
c	→	h(h(a,h(a,h(c,b))),f(f(h(h(a,h(h(f(a),c),f(c))),f(h(b,a))))))	(3)

The underlying signature is as follows:

{b/0, h/2, a/0, f/1, c/0}

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₀	=	h(h(a,c),b)
	→	h(h(a,c),h(h(b,a),f(a)))
	=	t₁

t₀	=	h(h(a,c),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:

{30}

transitions:

h(34,33)	→	35
h(35,32)	→	36
h(35,32)	→	34
h(155,154)	→	156
h(31,161)	→	162
h(32,37)	→	155
h(31,156)	→	157
h(157,153)	→	158
h(31,162)	→	163
h(163,160)	→	37
h(38,37)	→	39
h(39,36)	→	30
h(37,34)	→	161
c	→	37
a	→	31
a	→	33
a	→	38
b	→	34
f(37)	→	154
f(31)	→	32
f(35)	→	153
f(158)	→	159
f(159)	→	160

The automaton is closed under rewriting as it is compatible.

Automaton 2
- final states:
  
  {29}
- transitions:
  
  h(49,47) → 29
  
  h(29,48) → 49
  
  a → 46
  
  a → 48
  
  b → 29
  
  f(46) → 47
The automaton is closed under rewriting as it is compatible.