NO

The TRS could be proven non-terminating. The proof took 0 ms.

The rule 2ndspos(s(N), cons(X)) -> rcons(posrecip(Y), 2ndsneg(N, Z)) contains extra variables, thus the system is non-terminating.