Runtime Complexity TRS:
The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__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)
s(X) → n__s(X)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(X) → X

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

from'(X) → cons'(X, n__from'(n__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)
s'(X) → n__s'(X)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Sliced the following arguments:
cons'/0
cons2'/0
rcons'/0
posrecip'/0
negrecip'/0

Runtime Complexity TRS:
The TRS R consists of the following rules:

from'(X) → cons'(n__from'(n__s'(X)))
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(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)
s'(X) → n__s'(X)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
from'(X) → cons'(n__from'(n__s'(X)))
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(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)
s'(X) → n__s'(X)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Types:
from' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
cons' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
n__from' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
n__s' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
2ndspos' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2' → rnil':rcons'
0' :: n__s':n__from':cons':0':cons2'
rnil' :: rnil':rcons'
s' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
cons2' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
activate' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2' → rnil':rcons'
pi' :: n__s':n__from':cons':0':cons2' → rnil':rcons'
plus' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
times' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
square' :: n__s':n__from':cons':0':cons2' → n__s':n__from':cons':0':cons2'
_hole_n__s':n__from':cons':0':cons2'1 :: n__s':n__from':cons':0':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_gen_n__s':n__from':cons':0':cons2'3 :: Nat → n__s':n__from':cons':0':cons2'
_gen_rnil':rcons'4 :: Nat → rnil':rcons'

Heuristically decided to analyse the following defined symbols:
2ndspos', activate', 2ndsneg', plus', times'

They will be analysed ascendingly in the following order:
activate' < 2ndspos'
2ndspos' = 2ndsneg'
activate' < 2ndsneg'
plus' < times'

Generator Equations:
_gen_n__s':n__from':cons':0':cons2'3(0) ⇔ 0'
_gen_n__s':n__from':cons':0':cons2'3(+(x, 1)) ⇔ cons'(_gen_n__s':n__from':cons':0':cons2'3(x))
_gen_rnil':rcons'4(0) ⇔ rnil'
_gen_rnil':rcons'4(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'4(x))

The following defined symbols remain to be analysed:
activate', 2ndspos', 2ndsneg', plus', times'

They will be analysed ascendingly in the following order:
activate' < 2ndspos'
2ndspos' = 2ndsneg'
activate' < 2ndsneg'
plus' < times'

Could not prove a rewrite lemma for the defined symbol activate'.

The following defined symbols remain to be analysed:
plus', 2ndspos', 2ndsneg', times'

They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'
plus' < times'

Could not prove a rewrite lemma for the defined symbol plus'.

The following defined symbols remain to be analysed:
times', 2ndspos', 2ndsneg'

They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'

Could not prove a rewrite lemma for the defined symbol times'.

The following defined symbols remain to be analysed:
2ndsneg', 2ndspos'

They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'

Could not prove a rewrite lemma for the defined symbol 2ndsneg'.

The following defined symbols remain to be analysed:
2ndspos'

They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'

Could not prove a rewrite lemma for the defined symbol 2ndspos'.

No more defined symbols left to analyse.