Certification Problem

Input (COPS 954)

We consider the TRS containing the following rules:

sq(0(x)) p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))) (1)
sq(s(x)) s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x))))))))))))))))))))))))))))))))) (2)
twice(0(x)) p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))) (3)
twice(s(x)) p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x))))))))))))))) (4)
p(p(s(x))) p(x) (5)
p(s(x)) x (6)
p(0(x)) 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))) (7)
0(x) x (8)

The underlying signature is as follows:

{sq/1, 0/1, p/1, s/1, twice/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2023)

1 Non-Joinable Fork

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

t0 = sq(0(c_1))
p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(c_1)))))))))))))))))
p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(c_1)))))))))))))))
p(p(p(p(s(s(s(s(0(p(s(p(s(c_1)))))))))))))
p(p(p(p(s(s(s(s(0(p(s(c_1)))))))))))
= t4

t0 = sq(0(c_1))
sq(c_1)
= t1

The two resulting terms cannot be joined for the following reason: