Certification Problem

Input (TPDB TRS_Innermost/Mixed_innermost/tricky1)

The rewrite relation of the following TRS is considered.

f(g(x),g(y))	→	f(p(f(g(x),s(y))),g(s(p(x))))	(1)
p(0)	→	g(0)	(2)
g(s(p(x)))	→	p(x)	(3)

The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(g(x),g(y))	→	f^#(p(f(g(x),s(y))),g(s(p(x))))	(4)
f^#(g(x),g(y))	→	p^#(f(g(x),s(y)))	(5)
f^#(g(x),g(y))	→	f^#(g(x),s(y))	(6)
f^#(g(x),g(y))	→	g^#(s(p(x)))	(7)
f^#(g(x),g(y))	→	p^#(x)	(8)
p^#(0)	→	g^#(0)	(9)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.