We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
  , f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Arguments of following rules are not normal-forms:

{ f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) }

All above mentioned rules can be savely removed.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following dependency tuples:

Strict DPs:
  { f^#(cons(nil(), y)) -> c_1()
  , copy^#(0(), y, z) -> c_2(f^#(z))
  , copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { f^#(cons(nil(), y)) -> c_1()
  , copy^#(0(), y, z) -> c_2(f^#(z))
  , copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
Weak Trs:
  { f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {1} by applications of
Pre({1}) = {2,3}. Here rules are labeled as follows:

  DPs:
    { 1: f^#(cons(nil(), y)) -> c_1()
    , 2: copy^#(0(), y, z) -> c_2(f^#(z))
    , 3: copy^#(s(x), y, z) ->
         c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { copy^#(0(), y, z) -> c_2(f^#(z))
  , copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
Weak DPs: { f^#(cons(nil(), y)) -> c_1() }
Weak Trs:
  { f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {1} by applications of
Pre({1}) = {2}. Here rules are labeled as follows:

  DPs:
    { 1: copy^#(0(), y, z) -> c_2(f^#(z))
    , 2: copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y))
    , 3: f^#(cons(nil(), y)) -> c_1() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
Weak DPs:
  { f^#(cons(nil(), y)) -> c_1()
  , copy^#(0(), y, z) -> c_2(f^#(z)) }
Weak Trs:
  { f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ f^#(cons(nil(), y)) -> c_1()
, copy^#(0(), y, z) -> c_2(f^#(z)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
Weak Trs:
  { f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
Weak Trs:
  { f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Weak Usable Rules: { f(cons(nil(), y)) -> y }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
Weak Trs: { f(cons(nil(), y)) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.

DPs:
  { 1: copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }

Sub-proof:
----------
  The input was oriented with the instance of 'Small Polynomial Path
  Order (PS,1-bounded)' as induced by the safe mapping
  
   safe(f) = {}, safe(cons) = {1, 2}, safe(nil) = {}, safe(s) = {1},
   safe(copy^#) = {2, 3}, safe(c_1) = {}
  
  and precedence
  
   empty .
  
  Following symbols are considered recursive:
  
   {copy^#}
  
  The recursion depth is 1.
  
  Further, following argument filtering is employed:
  
   pi(f) = [], pi(cons) = [], pi(nil) = [], pi(s) = [1],
   pi(copy^#) = [1], pi(c_1) = [1]
  
  Usable defined function symbols are a subset of:
  
   {copy^#}
  
  For your convenience, here are the satisfied ordering constraints:
  
    pi(copy^#(s(x), y, z)) = copy^#(s(; x);)                     
                           > c_1(copy^#(x;);)                    
                           = pi(c_1(copy^#(x, y, cons(f(y), z))))
                                                                 

The strictly oriented rules are moved into the weak component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
  { copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
Weak Trs: { f(cons(nil(), y)) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs: { f(cons(nil(), y)) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))