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

Strict Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y
  , div(x, y) -> quot(x, y, y)
  , div(0(), y) -> 0()
  , div(div(x, y), z) -> div(x, times(y, z))
  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
  , quot(0(), s(y), z) -> 0()
  , quot(s(x), s(y), z) -> quot(x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

Arguments of following rules are not normal-forms:

{ div(div(x, y), z) -> div(x, times(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^2)).

Strict Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y
  , div(x, y) -> quot(x, y, y)
  , div(0(), y) -> 0()
  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
  , quot(0(), s(y), z) -> 0()
  , quot(s(x), s(y), z) -> quot(x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add the following dependency tuples:

Strict DPs:
  { plus^#(x, 0()) -> c_1()
  , plus^#(0(), y) -> c_2()
  , plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(0(), y) -> c_4()
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
  , times^#(s(0()), y) -> c_6()
  , div^#(x, y) -> c_7(quot^#(x, y, y))
  , div^#(0(), y) -> c_8()
  , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , quot^#(0(), s(y), z) -> c_10()
  , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }

and mark the set of starting terms.

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

Strict DPs:
  { plus^#(x, 0()) -> c_1()
  , plus^#(0(), y) -> c_2()
  , plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(0(), y) -> c_4()
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
  , times^#(s(0()), y) -> c_6()
  , div^#(x, y) -> c_7(quot^#(x, y, y))
  , div^#(0(), y) -> c_8()
  , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , quot^#(0(), s(y), z) -> c_10()
  , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y
  , div(x, y) -> quot(x, y, y)
  , div(0(), y) -> 0()
  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
  , quot(0(), s(y), z) -> 0()
  , quot(s(x), s(y), z) -> quot(x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We estimate the number of application of {1,2,4,6,8,10} by
applications of Pre({1,2,4,6,8,10}) = {3,5,7,9,11}. Here rules are
labeled as follows:

  DPs:
    { 1: plus^#(x, 0()) -> c_1()
    , 2: plus^#(0(), y) -> c_2()
    , 3: plus^#(s(x), y) -> c_3(plus^#(x, y))
    , 4: times^#(0(), y) -> c_4()
    , 5: times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
    , 6: times^#(s(0()), y) -> c_6()
    , 7: div^#(x, y) -> c_7(quot^#(x, y, y))
    , 8: div^#(0(), y) -> c_8()
    , 9: quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
    , 10: quot^#(0(), s(y), z) -> c_10()
    , 11: quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }

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

Strict DPs:
  { plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
  , div^#(x, y) -> c_7(quot^#(x, y, y))
  , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }
Weak DPs:
  { plus^#(x, 0()) -> c_1()
  , plus^#(0(), y) -> c_2()
  , times^#(0(), y) -> c_4()
  , times^#(s(0()), y) -> c_6()
  , div^#(0(), y) -> c_8()
  , quot^#(0(), s(y), z) -> c_10() }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y
  , div(x, y) -> quot(x, y, y)
  , div(0(), y) -> 0()
  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
  , quot(0(), s(y), z) -> 0()
  , quot(s(x), s(y), z) -> quot(x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

{ plus^#(x, 0()) -> c_1()
, plus^#(0(), y) -> c_2()
, times^#(0(), y) -> c_4()
, times^#(s(0()), y) -> c_6()
, div^#(0(), y) -> c_8()
, quot^#(0(), s(y), z) -> c_10() }

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

Strict DPs:
  { plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
  , div^#(x, y) -> c_7(quot^#(x, y, y))
  , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y
  , div(x, y) -> quot(x, y, y)
  , div(0(), y) -> 0()
  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
  , quot(0(), s(y), z) -> 0()
  , quot(s(x), s(y), z) -> quot(x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { plus(x, 0()) -> x
    , plus(0(), y) -> y
    , plus(s(x), y) -> s(plus(x, y))
    , times(0(), y) -> 0()
    , times(s(x), y) -> plus(y, times(x, y))
    , times(s(0()), y) -> y }

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

Strict DPs:
  { plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
  , div^#(x, y) -> c_7(quot^#(x, y, y))
  , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 5: quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_7) = {1},
    Uargs(c_9) = {1}, Uargs(c_11) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
          [plus](x1, x2) = [0]                  
                                                
                     [0] = [0]                  
                                                
                 [s](x1) = [1] x1 + [2]         
                                                
         [times](x1, x2) = [0]                  
                                                
        [plus^#](x1, x2) = [0]                  
                                                
               [c_3](x1) = [4] x1 + [0]         
                                                
       [times^#](x1, x2) = [0]                  
                                                
           [c_5](x1, x2) = [4] x1 + [4] x2 + [0]
                                                
         [div^#](x1, x2) = [4] x1 + [4] x2 + [1]
                                                
               [c_7](x1) = [1] x1 + [0]         
                                                
    [quot^#](x1, x2, x3) = [4] x1 + [4] x3 + [1]
                                                
               [c_9](x1) = [1] x1 + [0]         
                                                
              [c_11](x1) = [1] x1 + [6]         
  
  The order satisfies the following ordering constraints:
  
             [plus(x, 0())] =  [0]                                         
                            ?  [1] x + [0]                                 
                            =  [x]                                         
                                                                           
             [plus(0(), y)] =  [0]                                         
                            ?  [1] y + [0]                                 
                            =  [y]                                         
                                                                           
            [plus(s(x), y)] =  [0]                                         
                            ?  [2]                                         
                            =  [s(plus(x, y))]                             
                                                                           
            [times(0(), y)] =  [0]                                         
                            >= [0]                                         
                            =  [0()]                                       
                                                                           
           [times(s(x), y)] =  [0]                                         
                            >= [0]                                         
                            =  [plus(y, times(x, y))]                      
                                                                           
         [times(s(0()), y)] =  [0]                                         
                            ?  [1] y + [0]                                 
                            =  [y]                                         
                                                                           
          [plus^#(s(x), y)] =  [0]                                         
                            >= [0]                                         
                            =  [c_3(plus^#(x, y))]                         
                                                                           
         [times^#(s(x), y)] =  [0]                                         
                            >= [0]                                         
                            =  [c_5(plus^#(y, times(x, y)), times^#(x, y))]
                                                                           
              [div^#(x, y)] =  [4] x + [4] y + [1]                         
                            >= [4] x + [4] y + [1]                         
                            =  [c_7(quot^#(x, y, y))]                      
                                                                           
     [quot^#(x, 0(), s(z))] =  [4] x + [4] z + [9]                         
                            >= [4] x + [4] z + [9]                         
                            =  [c_9(div^#(x, s(z)))]                       
                                                                           
    [quot^#(s(x), s(y), z)] =  [4] x + [4] z + [9]                         
                            >  [4] x + [4] z + [7]                         
                            =  [c_11(quot^#(x, y, z))]                     
                                                                           

We return to the main proof. Consider the set of all dependency
pairs

:
  { 1: plus^#(s(x), y) -> c_3(plus^#(x, y))
  , 2: times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y))
  , 3: div^#(x, y) -> c_7(quot^#(x, y, y))
  , 4: quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , 5: quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {5}. These cover all (indirect) predecessors of dependency
pairs {3,4,5}, their number of application is equally bounded. The
dependency pairs are shifted into the weak component.

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

Strict DPs:
  { plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) }
Weak DPs:
  { div^#(x, y) -> c_7(quot^#(x, y, y))
  , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
  , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

{ div^#(x, y) -> c_7(quot^#(x, y, y))
, quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z)))
, quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) }

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

Strict DPs:
  { plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

DPs:
  { 1: plus^#(s(x), y) -> c_3(plus^#(x, y))
  , 2: times^#(s(x), y) ->
       c_5(plus^#(y, times(x, y)), times^#(x, y)) }

Sub-proof:
----------
  The input was oriented with the instance of 'Small Polynomial Path
  Order (PS,2-bounded)' as induced by the safe mapping
  
   safe(plus) = {}, safe(0) = {}, safe(s) = {1}, safe(times) = {},
   safe(plus^#) = {2}, safe(c_3) = {}, safe(times^#) = {},
   safe(c_5) = {}, safe(div^#) = {}, safe(c_7) = {},
   safe(quot^#) = {}, safe(c_9) = {}, safe(c_11) = {}
  
  and precedence
  
   times > plus, times^# > plus^# .
  
  Following symbols are considered recursive:
  
   {plus^#, times^#}
  
  The recursion depth is 2.
  
  Further, following argument filtering is employed:
  
   pi(plus) = [1, 2], pi(0) = [], pi(s) = [1], pi(times) = [],
   pi(plus^#) = [1], pi(c_3) = [1], pi(times^#) = [1, 2],
   pi(c_5) = [1, 2], pi(div^#) = [], pi(c_7) = [], pi(quot^#) = [],
   pi(c_9) = [], pi(c_11) = []
  
  Usable defined function symbols are a subset of:
  
   {plus^#, times^#, div^#, quot^#}
  
  For your convenience, here are the satisfied ordering constraints:
  
     pi(plus^#(s(x), y)) = plus^#(s(; x);)                               
                         > c_3(plus^#(x;);)                              
                         = pi(c_3(plus^#(x, y)))                         
                                                                         
    pi(times^#(s(x), y)) = times^#(s(; x),  y;)                          
                         > c_5(plus^#(y;),  times^#(x,  y;);)            
                         = pi(c_5(plus^#(y, times(x, y)), times^#(x, y)))
                                                                         

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:
  { plus^#(s(x), y) -> c_3(plus^#(x, y))
  , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) }
Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), 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.

{ plus^#(s(x), y) -> c_3(plus^#(x, y))
, times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) }

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

Weak Trs:
  { plus(x, 0()) -> x
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , times(0(), y) -> 0()
  , times(s(x), y) -> plus(y, times(x, y))
  , times(s(0()), 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^2))