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

t(N) → cs(r(q(N)), nt(ns(N)))
q(0) → 0
q(s(X)) → s(p(q(X), d(X)))
d(0) → 0
d(s(X)) → s(s(d(X)))
p(0, X) → X
p(X, 0) → X
p(s(X), s(Y)) → s(s(p(X, Y)))
f(0, X) → nil
f(s(X), cs(Y, Z)) → cs(Y, nf(X, a(Z)))
t(X) → nt(X)
s(X) → ns(X)
f(X1, X2) → nf(X1, X2)
a(nt(X)) → t(a(X))
a(ns(X)) → s(a(X))
a(nf(X1, X2)) → f(a(X1), a(X2))
a(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:

t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'

Heuristically decided to analyse the following defined symbols:
q', p', d', a'

They will be analysed ascendingly in the following order:
p' < q'
d' < q'

Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'

Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))

The following defined symbols remain to be analysed:
p', q', d', a'

They will be analysed ascendingly in the following order:
p' < q'
d' < q'

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

Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'

Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))

The following defined symbols remain to be analysed:
d', q', a'

They will be analysed ascendingly in the following order:
d' < q'

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

Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'

Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))

The following defined symbols remain to be analysed:
q', a'

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

Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'

Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))

The following defined symbols remain to be analysed:
a'

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

Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X

Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'

Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))

No more defined symbols left to analyse.