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}

Prove or disprove confluence.

No.

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

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

When applying the cap-function on both terms (where variables may be treated like constants) then the resulting terms do not unify.