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

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'(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

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

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

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

Rewrite Strategy: INNERMOST

Infered types.

Rules:
from'cons'(n__from')
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')
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'n__from'
activate'(n__from') → from'
activate'(X) → X

Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'

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

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

Rules:
from'cons'(n__from')
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')
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'n__from'
activate'(n__from') → from'
activate'(X) → X

Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'

Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))

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'

Proved the following rewrite lemma:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)

Induction Base:
plus'(_gen_0':s'6(0), _gen_0':s'6(b)) →RΩ(1)
_gen_0':s'6(b)

Induction Step:
plus'(_gen_0':s'6(+(_\$n9, 1)), _gen_0':s'6(_b321)) →RΩ(1)
s'(plus'(_gen_0':s'6(_\$n9), _gen_0':s'6(_b321))) →IH
s'(_gen_0':s'6(+(_\$n9, _b321)))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
from'cons'(n__from')
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')
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'n__from'
activate'(n__from') → from'
activate'(X) → X

Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'

Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)

Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))

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

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

Proved the following rewrite lemma:
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)

Induction Base:
times'(_gen_0':s'6(0), _gen_0':s'6(b)) →RΩ(1)
0'

Induction Step:
times'(_gen_0':s'6(+(_\$n1034, 1)), _gen_0':s'6(_b1581)) →RΩ(1)
plus'(_gen_0':s'6(_b1581), times'(_gen_0':s'6(_\$n1034), _gen_0':s'6(_b1581))) →IH
plus'(_gen_0':s'6(_b1581), _gen_0':s'6(*(_\$n1034, _b1581))) →LΩ(1 + b1581)
_gen_0':s'6(+(_b1581, *(_\$n1034, _b1581)))

We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).

Rules:
from'cons'(n__from')
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')
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'n__from'
activate'(n__from') → from'
activate'(X) → X

Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'

Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)

Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))

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 conjecture could not be proven:

2ndsneg'(_gen_0':s'6(_n2566), _gen_n__from':cons':cons2'4(1)) →? _gen_rnil':rcons'5(_n2566)

Rules:
from'cons'(n__from')
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')
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'n__from'
activate'(n__from') → from'
activate'(X) → X

Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'

Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)

Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))

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'.

The following conjecture could not be proven:

2ndspos'(_gen_0':s'6(_n10278), _gen_n__from':cons':cons2'4(1)) →? _gen_rnil':rcons'5(_n10278)

Rules:
from'cons'(n__from')
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')
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'n__from'
activate'(n__from') → from'
activate'(X) → X

Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'

Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)

Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)