YES

The TRS could be proven terminating. The proof took 22 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (10ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

prime(0)	→	false		prime(s(0))	→	false
prime(s(s(x)))	→	prime1(s(s(x)), s(x))		prime1(x, 0)	→	false
prime1(x, s(0))	→	true		prime1(x, s(s(y)))	→	and(not(divp(s(s(y)), x)), prime1(x, s(y)))
divp(x, y)	→	=(rem(x, y), 0)

Original Signature

Termination of terms over the following signature is verified: prime, not, 0, divp, s, rem, false, prime1, true, =, and

Strategy

The following SCCs where found

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

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

→

prime1^#(x, s(y))

Rewrite Rules

prime(0)	→	false		prime(s(0))	→	false
prime(s(s(x)))	→	prime1(s(s(x)), s(x))		prime1(x, 0)	→	false
prime1(x, s(0))	→	true		prime1(x, s(s(y)))	→	and(not(divp(s(s(y)), x)), prime1(x, s(y)))
divp(x, y)	→	=(rem(x, y), 0)

Original Signature

Termination of terms over the following signature is verified: prime, not, 0, divp, s, rem, false, prime1, true, =, and

Strategy

Projection

The following projection was used:

π (prime1#): 2

Thus, the following dependency pairs are removed:

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

→

prime1^#(x, s(y))