YES(O(1),O(n^1))

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

Strict Trs:
  { ordered(Cons(x', Cons(x, xs))) ->
    ordered[Ite][True][Ite][True][Ite](<(x', x),
                                       Cons(x', Cons(x, xs)))
  , ordered(Cons(x, Nil())) -> True()
  , ordered(Nil()) -> True()
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> ordered(xs) }
Weak Trs:
  { <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following innermost weak dependency pairs:

Strict DPs:
  { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x))
  , ordered^#(Cons(x, Nil())) -> c_2()
  , ordered^#(Nil()) -> c_3()
  , notEmpty^#(Cons(x, xs)) -> c_4()
  , notEmpty^#(Nil()) -> c_5()
  , goal^#(xs) -> c_6(ordered^#(xs)) }
Weak DPs:
  { <^#(x, 0()) -> c_7()
  , <^#(S(x), S(y)) -> c_8(<^#(x, y))
  , <^#(0(), S(y)) -> c_9() }

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:
  { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x))
  , ordered^#(Cons(x, Nil())) -> c_2()
  , ordered^#(Nil()) -> c_3()
  , notEmpty^#(Cons(x, xs)) -> c_4()
  , notEmpty^#(Nil()) -> c_5()
  , goal^#(xs) -> c_6(ordered^#(xs)) }
Strict Trs:
  { ordered(Cons(x', Cons(x, xs))) ->
    ordered[Ite][True][Ite][True][Ite](<(x', x),
                                       Cons(x', Cons(x, xs)))
  , ordered(Cons(x, Nil())) -> True()
  , ordered(Nil()) -> True()
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> ordered(xs) }
Weak DPs:
  { <^#(x, 0()) -> c_7()
  , <^#(S(x), S(y)) -> c_8(<^#(x, y))
  , <^#(0(), S(y)) -> c_9() }
Weak Trs:
  { <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^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(n^1)).

Strict DPs:
  { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x))
  , ordered^#(Cons(x, Nil())) -> c_2()
  , ordered^#(Nil()) -> c_3()
  , notEmpty^#(Cons(x, xs)) -> c_4()
  , notEmpty^#(Nil()) -> c_5()
  , goal^#(xs) -> c_6(ordered^#(xs)) }
Weak DPs:
  { <^#(x, 0()) -> c_7()
  , <^#(S(x), S(y)) -> c_8(<^#(x, y))
  , <^#(0(), S(y)) -> c_9() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(c_1) = {1}, Uargs(c_6) = {1}, Uargs(c_8) = {1}

TcT has computed the following constructor-restricted matrix
interpretation.

           [S](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
    [Cons](x1, x2) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
             [Nil] = [0]           
                     [0]           
                                   
               [0] = [0]           
                     [0]           
                                   
   [ordered^#](x1) = [1]           
                     [0]           
                                   
         [c_1](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
  [<^#](x1, x2) = [0]           
                     [0]           
                                   
             [c_2] = [0]           
                     [0]           
                                   
             [c_3] = [0]           
                     [0]           
                                   
  [notEmpty^#](x1) = [1 1] x1 + [2]
                     [1 1]      [2]
                                   
             [c_4] = [1]           
                     [1]           
                                   
             [c_5] = [1]           
                     [2]           
                                   
      [goal^#](x1) = [2 1] x1 + [2]
                     [2 1]      [2]
                                   
         [c_6](x1) = [1 0] x1 + [0]
                     [0 1]      [2]
                                   
             [c_7] = [0]           
                     [0]           
                                   
         [c_8](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
             [c_9] = [0]           
                     [0]           

The following symbols are considered usable

  {ordered^#, <^#, notEmpty^#, goal^#}

The order satisfies the following ordering constraints:

  [ordered^#(Cons(x', Cons(x, xs)))] =  [1]                 
                                        [0]                 
                                     >  [0]                 
                                        [0]                 
                                     =  [c_1(<^#(x', x))]
                                                            
         [ordered^#(Cons(x, Nil()))] =  [1]                 
                                        [0]                 
                                     >  [0]                 
                                        [0]                 
                                     =  [c_2()]             
                                                            
                  [ordered^#(Nil())] =  [1]                 
                                        [0]                 
                                     >  [0]                 
                                        [0]                 
                                     =  [c_3()]             
                                                            
                    [<^#(x, 0())] =  [0]                 
                                        [0]                 
                                     >= [0]                 
                                        [0]                 
                                     =  [c_7()]             
                                                            
                [<^#(S(x), S(y))] =  [0]                 
                                        [0]                 
                                     >= [0]                 
                                        [0]                 
                                     =  [c_8(<^#(x, y))] 
                                                            
                 [<^#(0(), S(y))] =  [0]                 
                                        [0]                 
                                     >= [0]                 
                                        [0]                 
                                     =  [c_9()]             
                                                            
           [notEmpty^#(Cons(x, xs))] =  [1 0] x + [2]       
                                        [1 0]     [2]       
                                     >  [1]                 
                                        [1]                 
                                     =  [c_4()]             
                                                            
                 [notEmpty^#(Nil())] =  [2]                 
                                        [2]                 
                                     >  [1]                 
                                        [2]                 
                                     =  [c_5()]             
                                                            
                        [goal^#(xs)] =  [2 1] xs + [2]      
                                        [2 1]      [2]      
                                     >  [1]                 
                                        [2]                 
                                     =  [c_6(ordered^#(xs))]
                                                            

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

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

Weak DPs:
  { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x))
  , ordered^#(Cons(x, Nil())) -> c_2()
  , ordered^#(Nil()) -> c_3()
  , <^#(x, 0()) -> c_7()
  , <^#(S(x), S(y)) -> c_8(<^#(x, y))
  , <^#(0(), S(y)) -> c_9()
  , notEmpty^#(Cons(x, xs)) -> c_4()
  , notEmpty^#(Nil()) -> c_5()
  , goal^#(xs) -> c_6(ordered^#(xs)) }
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.

{ ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x))
, ordered^#(Cons(x, Nil())) -> c_2()
, ordered^#(Nil()) -> c_3()
, <^#(x, 0()) -> c_7()
, <^#(S(x), S(y)) -> c_8(<^#(x, y))
, <^#(0(), S(y)) -> c_9()
, notEmpty^#(Cons(x, xs)) -> c_4()
, notEmpty^#(Nil()) -> c_5()
, goal^#(xs) -> c_6(ordered^#(xs)) }

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))