Certification Problem

Input (TPDB TRS_Standard/SK90/2.29)

The rewrite relation of the following TRS is considered.

prime(0)	→	false	(1)
prime(s(0))	→	false	(2)
prime(s(s(x)))	→	prime1(s(s(x)),s(x))	(3)
prime1(x,0)	→	false	(4)
prime1(x,s(0))	→	true	(5)
prime1(x,s(s(y)))	→	and(not(divp(s(s(y)),x)),prime1(x,s(y)))	(6)
divp(x,y)	→	=(rem(x,y),0)	(7)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

prime^#(s(s(x)))	→	prime1^#(s(s(x)),s(x))	(8)
prime1^#(x,s(s(y)))	→	prime1^#(x,s(y))	(9)
prime1^#(x,s(s(y)))	→	divp^#(s(s(y)),x)	(10)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair
prime1^#(x,s(s(y))) → prime1^#(x,s(y)) (9)

1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

prime1^#(x,s(s(y))) → prime1^#(x,s(y)) (9)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.