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

a__from(X) → cons(mark(X), from(s(X)))
a__2ndspos(0, Z) → rnil
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__plus(0, Y) → mark(Y)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__times(0, Y) → 0
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__square(X) → a__times(mark(X), mark(X))
mark(from(X)) → a__from(mark(X))
mark(2ndspos(X1, X2)) → a__2ndspos(mark(X1), mark(X2))
mark(2ndsneg(X1, X2)) → a__2ndsneg(mark(X1), mark(X2))
mark(pi(X)) → a__pi(mark(X))
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
mark(square(X)) → a__square(mark(X))
mark(0) → 0
mark(s(X)) → s(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
mark(negrecip(X)) → negrecip(mark(X))
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
mark(rnil) → rnil
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
a__from(X) → from(X)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__times(X1, X2) → times(X1, X2)
a__square(X) → square(X)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a__from'(X) → cons'(mark'(X), from'(s'(X)))
a__2ndspos'(0', Z) → rnil'
a__2ndspos'(s'(N), cons'(X, Z)) → a__2ndspos'(s'(mark'(N)), cons2'(X, mark'(Z)))
a__2ndspos'(s'(N), cons2'(X, cons'(Y, Z))) → rcons'(posrecip'(mark'(Y)), a__2ndsneg'(mark'(N), mark'(Z)))
a__2ndsneg'(0', Z) → rnil'
a__2ndsneg'(s'(N), cons'(X, Z)) → a__2ndsneg'(s'(mark'(N)), cons2'(X, mark'(Z)))
a__2ndsneg'(s'(N), cons2'(X, cons'(Y, Z))) → rcons'(negrecip'(mark'(Y)), a__2ndspos'(mark'(N), mark'(Z)))
a__pi'(X) → a__2ndspos'(mark'(X), a__from'(0'))
a__plus'(0', Y) → mark'(Y)
a__plus'(s'(X), Y) → s'(a__plus'(mark'(X), mark'(Y)))
a__times'(0', Y) → 0'
a__times'(s'(X), Y) → a__plus'(mark'(Y), a__times'(mark'(X), mark'(Y)))
a__square'(X) → a__times'(mark'(X), mark'(X))
mark'(from'(X)) → a__from'(mark'(X))
mark'(2ndspos'(X1, X2)) → a__2ndspos'(mark'(X1), mark'(X2))
mark'(2ndsneg'(X1, X2)) → a__2ndsneg'(mark'(X1), mark'(X2))
mark'(pi'(X)) → a__pi'(mark'(X))
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(times'(X1, X2)) → a__times'(mark'(X1), mark'(X2))
mark'(square'(X)) → a__square'(mark'(X))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(posrecip'(X)) → posrecip'(mark'(X))
mark'(negrecip'(X)) → negrecip'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(cons2'(X1, X2)) → cons2'(X1, mark'(X2))
mark'(rnil') → rnil'
mark'(rcons'(X1, X2)) → rcons'(mark'(X1), mark'(X2))
a__from'(X) → from'(X)
a__2ndspos'(X1, X2) → 2ndspos'(X1, X2)
a__2ndsneg'(X1, X2) → 2ndsneg'(X1, X2)
a__pi'(X) → pi'(X)
a__plus'(X1, X2) → plus'(X1, X2)
a__times'(X1, X2) → times'(X1, X2)
a__square'(X) → square'(X)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
cons2'/0

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

a__from'(X) → cons'(mark'(X), from'(s'(X)))
a__2ndspos'(0', Z) → rnil'
a__2ndspos'(s'(N), cons'(X, Z)) → a__2ndspos'(s'(mark'(N)), cons2'(mark'(Z)))
a__2ndspos'(s'(N), cons2'(cons'(Y, Z))) → rcons'(posrecip'(mark'(Y)), a__2ndsneg'(mark'(N), mark'(Z)))
a__2ndsneg'(0', Z) → rnil'
a__2ndsneg'(s'(N), cons'(X, Z)) → a__2ndsneg'(s'(mark'(N)), cons2'(mark'(Z)))
a__2ndsneg'(s'(N), cons2'(cons'(Y, Z))) → rcons'(negrecip'(mark'(Y)), a__2ndspos'(mark'(N), mark'(Z)))
a__pi'(X) → a__2ndspos'(mark'(X), a__from'(0'))
a__plus'(0', Y) → mark'(Y)
a__plus'(s'(X), Y) → s'(a__plus'(mark'(X), mark'(Y)))
a__times'(0', Y) → 0'
a__times'(s'(X), Y) → a__plus'(mark'(Y), a__times'(mark'(X), mark'(Y)))
a__square'(X) → a__times'(mark'(X), mark'(X))
mark'(from'(X)) → a__from'(mark'(X))
mark'(2ndspos'(X1, X2)) → a__2ndspos'(mark'(X1), mark'(X2))
mark'(2ndsneg'(X1, X2)) → a__2ndsneg'(mark'(X1), mark'(X2))
mark'(pi'(X)) → a__pi'(mark'(X))
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(times'(X1, X2)) → a__times'(mark'(X1), mark'(X2))
mark'(square'(X)) → a__square'(mark'(X))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(posrecip'(X)) → posrecip'(mark'(X))
mark'(negrecip'(X)) → negrecip'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(cons2'(X2)) → cons2'(mark'(X2))
mark'(rnil') → rnil'
mark'(rcons'(X1, X2)) → rcons'(mark'(X1), mark'(X2))
a__from'(X) → from'(X)
a__2ndspos'(X1, X2) → 2ndspos'(X1, X2)
a__2ndsneg'(X1, X2) → 2ndsneg'(X1, X2)
a__pi'(X) → pi'(X)
a__plus'(X1, X2) → plus'(X1, X2)
a__times'(X1, X2) → times'(X1, X2)
a__square'(X) → square'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__from'(X) → cons'(mark'(X), from'(s'(X)))
a__2ndspos'(0', Z) → rnil'
a__2ndspos'(s'(N), cons'(X, Z)) → a__2ndspos'(s'(mark'(N)), cons2'(mark'(Z)))
a__2ndspos'(s'(N), cons2'(cons'(Y, Z))) → rcons'(posrecip'(mark'(Y)), a__2ndsneg'(mark'(N), mark'(Z)))
a__2ndsneg'(0', Z) → rnil'
a__2ndsneg'(s'(N), cons'(X, Z)) → a__2ndsneg'(s'(mark'(N)), cons2'(mark'(Z)))
a__2ndsneg'(s'(N), cons2'(cons'(Y, Z))) → rcons'(negrecip'(mark'(Y)), a__2ndspos'(mark'(N), mark'(Z)))
a__pi'(X) → a__2ndspos'(mark'(X), a__from'(0'))
a__plus'(0', Y) → mark'(Y)
a__plus'(s'(X), Y) → s'(a__plus'(mark'(X), mark'(Y)))
a__times'(0', Y) → 0'
a__times'(s'(X), Y) → a__plus'(mark'(Y), a__times'(mark'(X), mark'(Y)))
a__square'(X) → a__times'(mark'(X), mark'(X))
mark'(from'(X)) → a__from'(mark'(X))
mark'(2ndspos'(X1, X2)) → a__2ndspos'(mark'(X1), mark'(X2))
mark'(2ndsneg'(X1, X2)) → a__2ndsneg'(mark'(X1), mark'(X2))
mark'(pi'(X)) → a__pi'(mark'(X))
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(times'(X1, X2)) → a__times'(mark'(X1), mark'(X2))
mark'(square'(X)) → a__square'(mark'(X))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(posrecip'(X)) → posrecip'(mark'(X))
mark'(negrecip'(X)) → negrecip'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(cons2'(X2)) → cons2'(mark'(X2))
mark'(rnil') → rnil'
mark'(rcons'(X1, X2)) → rcons'(mark'(X1), mark'(X2))
a__from'(X) → from'(X)
a__2ndspos'(X1, X2) → 2ndspos'(X1, X2)
a__2ndsneg'(X1, X2) → 2ndsneg'(X1, X2)
a__pi'(X) → pi'(X)
a__plus'(X1, X2) → plus'(X1, X2)
a__times'(X1, X2) → times'(X1, X2)
a__square'(X) → square'(X)

Types:
a__from' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
cons' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
mark' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
from' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
s' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
a__2ndspos' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
0' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
rnil' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
cons2' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
rcons' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
posrecip' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
a__2ndsneg' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
negrecip' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
a__pi' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
a__plus' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
a__times' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
a__square' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
2ndspos' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
2ndsneg' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
pi' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
plus' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
times' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
square' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil' → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
nil' :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
_hole_s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'1 :: s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'
_gen_s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'2 :: Nat → s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'

Heuristically decided to analyse the following defined symbols:
a__from', mark', a__2ndspos', a__2ndsneg', a__pi', a__plus', a__times', a__square'

They will be analysed ascendingly in the following order:
a__from' = mark'
a__from' = a__2ndspos'
a__from' = a__2ndsneg'
a__from' = a__pi'
a__from' = a__plus'
a__from' = a__times'
a__from' = a__square'
mark' = a__2ndspos'
mark' = a__2ndsneg'
mark' = a__pi'
mark' = a__plus'
mark' = a__times'
mark' = a__square'
a__2ndspos' = a__2ndsneg'
a__2ndspos' = a__pi'
a__2ndspos' = a__plus'
a__2ndspos' = a__times'
a__2ndspos' = a__square'
a__2ndsneg' = a__pi'
a__2ndsneg' = a__plus'
a__2ndsneg' = a__times'
a__2ndsneg' = a__square'
a__pi' = a__plus'
a__pi' = a__times'
a__pi' = a__square'
a__plus' = a__times'
a__plus' = a__square'
a__times' = a__square'

Generator Equations:
_gen_s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'2(0) ⇔ 0'
_gen_s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'2(+(x, 1)) ⇔ cons'(0', _gen_s':from':cons':0':rnil':cons2':posrecip':rcons':negrecip':2ndspos':2ndsneg':pi':plus':times':square':nil'2(x))

The following defined symbols remain to be analysed:
mark', a__from', a__2ndspos', a__2ndsneg', a__pi', a__plus', a__times', a__square'

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

The following defined symbols remain to be analysed:
a__from', a__2ndspos', a__2ndsneg', a__pi', a__plus', a__times', a__square'

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

The following defined symbols remain to be analysed:
a__2ndspos', a__2ndsneg', a__pi', a__plus', a__times', a__square'

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

The following defined symbols remain to be analysed:
a__2ndsneg', a__pi', a__plus', a__times', a__square'

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

The following defined symbols remain to be analysed:
a__pi', a__plus', a__times', a__square'

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

The following defined symbols remain to be analysed:
a__plus', a__times', a__square'

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

The following defined symbols remain to be analysed:
a__times', a__square'

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

The following defined symbols remain to be analysed:
a__square'

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

No more defined symbols left to analyse.