(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
from(X) → cons(X, n__from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, activate(Z)))
2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, activate(Z)))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
activate(n__from(X)) → from(X)
activate(X) → X
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
2ndspos(s(s(N854_1)), cons(X, cons(Y288_1, cons2(X855_1, cons(Y856_1, Z857_1))))) →+ rcons(posrecip(Y288_1), rcons(negrecip(Y856_1), 2ndspos(N854_1, Z857_1)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1,1].
The pumping substitution is [N854_1 / s(s(N854_1)), Z857_1 / cons(X, cons(Y288_1, cons2(X855_1, cons(Y856_1, Z857_1))))].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)