YES

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (2ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

terms^#(N)

→

sqr^#(N)

Rewrite Rules

terms(N)	→	cons(recip(sqr(N)))		sqr(0)	→	0
sqr(s)	→	s		dbl(0)	→	0
dbl(s)	→	s		add(0, X)	→	X
add(s, Y)	→	s		first(0, X)	→	nil
first(s, cons(Y))	→	cons(Y)

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, cons, nil

Strategy

There are no SCCs!