Certification Problem

Input (TPDB TRS_Standard/AG01/#3.33)

The rewrite relation of the following TRS is considered.

p(f(f(x)))	→	q(f(g(x)))	(1)
p(g(g(x)))	→	q(g(f(x)))	(2)
q(f(f(x)))	→	p(f(g(x)))	(3)
q(g(g(x)))	→	p(g(f(x)))	(4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

q^#(f(f(x)))	→	p^#(f(g(x)))	(5)
p^#(f(f(x)))	→	q^#(f(g(x)))	(6)
p^#(g(g(x)))	→	q^#(g(f(x)))	(7)
q^#(g(g(x)))	→	p^#(g(f(x)))	(8)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.