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

f(cons(nil, y)) → y
f(cons(f(cons(nil, y)), z)) → copy(n, y, z)
copy(0, y, z) → f(z)
copy(s(x), y, z) → copy(x, y, cons(f(y), z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))

Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'

Heuristically decided to analyse the following defined symbols:
f', copy'

They will be analysed ascendingly in the following order:
f' = copy'

Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))

Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'

Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
_gen_n':0':s'4(0) ⇔ 0'
_gen_n':0':s'4(+(x, 1)) ⇔ s'(_gen_n':0':s'4(x))

The following defined symbols remain to be analysed:
copy', f'

They will be analysed ascendingly in the following order:
f' = copy'

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

The following conjecture could not be proven:

copy'(_gen_n':0':s'4(_n6), _gen_nil':cons'3(1), _gen_nil':cons'3(c)) →? _*5

Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))

Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'

Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
_gen_n':0':s'4(0) ⇔ 0'
_gen_n':0':s'4(+(x, 1)) ⇔ s'(_gen_n':0':s'4(x))

The following defined symbols remain to be analysed:
f'

They will be analysed ascendingly in the following order:
f' = copy'

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

Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))

Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'

Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
_gen_n':0':s'4(0) ⇔ 0'
_gen_n':0':s'4(+(x, 1)) ⇔ s'(_gen_n':0':s'4(x))

No more defined symbols left to analyse.