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

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

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

We add the following dependency tuples:

Strict DPs:
  { times^#(x, 0()) -> c_1()
  , times^#(x, s(y)) -> c_2(plus^#(times(x, y), x), times^#(x, y))
  , plus^#(x, 0()) -> c_3()
  , plus^#(x, s(y)) -> c_4(plus^#(x, y))
  , plus^#(0(), x) -> c_5()
  , plus^#(s(x), y) -> c_6(plus^#(x, 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^3)).

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

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

  DPs:
    { 1: times^#(x, 0()) -> c_1()
    , 2: times^#(x, s(y)) -> c_2(plus^#(times(x, y), x), times^#(x, y))
    , 3: plus^#(x, 0()) -> c_3()
    , 4: plus^#(x, s(y)) -> c_4(plus^#(x, y))
    , 5: plus^#(0(), x) -> c_5()
    , 6: plus^#(s(x), y) -> c_6(plus^#(x, y)) }

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

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

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

{ times^#(x, 0()) -> c_1()
, plus^#(x, 0()) -> c_3()
, plus^#(0(), x) -> c_5() }

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

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

We decompose the input problem according to the dependency graph
into the upper component

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

and lower component

  { plus^#(x, s(y)) -> c_4(plus^#(x, y))
  , plus^#(s(x), y) -> c_6(plus^#(x, y)) }

Further, following extension rules are added to the lower
component.

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

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { times^#(x, s(y)) -> c_2(plus^#(times(x, y), x), times^#(x, y)) }
  Weak Trs:
    { times(x, 0()) -> 0()
    , times(x, s(y)) -> plus(times(x, y), x)
    , plus(x, 0()) -> x
    , plus(x, s(y)) -> s(plus(x, y))
    , plus(0(), x) -> x
    , plus(s(x), y) -> s(plus(x, 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: times^#(x, s(y)) ->
         c_2(plus^#(times(x, y), x), times^#(x, y)) }
  Trs: { plus(0(), x) -> x }
  
  Sub-proof:
  ----------
    The input was oriented with the instance of 'Small Polynomial Path
    Order (PS,1-bounded)' as induced by the safe mapping
    
     safe(times) = {}, safe(0) = {}, safe(s) = {1}, safe(plus) = {},
     safe(times^#) = {1}, safe(c_1) = {}, safe(c_2) = {},
     safe(plus^#) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {},
     safe(c_6) = {}
    
    and precedence
    
     times > plus, times^# > plus .
    
    Following symbols are considered recursive:
    
     {times^#}
    
    The recursion depth is 1.
    
    Further, following argument filtering is employed:
    
     pi(times) = 1, pi(0) = [], pi(s) = [1], pi(plus) = [2],
     pi(times^#) = [2], pi(c_1) = [], pi(c_2) = [1, 2], pi(plus^#) = [],
     pi(c_3) = [], pi(c_4) = [], pi(c_5) = [], pi(c_6) = []
    
    Usable defined function symbols are a subset of:
    
     {times^#, plus^#}
    
    For your convenience, here are the satisfied ordering constraints:
    
      pi(times^#(x, s(y))) = times^#(s(; y);)                              
                           > c_2(plus^#(),  times^#(y;);)                  
                           = pi(c_2(plus^#(times(x, y), x), 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:
    { times^#(x, s(y)) -> c_2(plus^#(times(x, y), x), times^#(x, y)) }
  Weak Trs:
    { times(x, 0()) -> 0()
    , times(x, s(y)) -> plus(times(x, y), x)
    , plus(x, 0()) -> x
    , plus(x, s(y)) -> s(plus(x, y))
    , plus(0(), x) -> x
    , plus(s(x), y) -> s(plus(x, 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.
  
  { times^#(x, s(y)) -> c_2(plus^#(times(x, y), x), times^#(x, y)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { times(x, 0()) -> 0()
    , times(x, s(y)) -> plus(times(x, y), x)
    , plus(x, 0()) -> x
    , plus(x, s(y)) -> s(plus(x, y))
    , plus(0(), x) -> x
    , plus(s(x), y) -> s(plus(x, 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

We return to the main proof.

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

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

We use the processor 'polynomial interpretation' to orient
following rules strictly.

DPs:
  { 1: plus^#(x, s(y)) -> c_4(plus^#(x, y))
  , 4: times^#(x, s(y)) -> plus^#(times(x, y), x) }

Sub-proof:
----------
  The following argument positions are considered usable:
  
    Uargs(c_4) = {1}, Uargs(c_6) = {1}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
    [times](x1, x2) = 0                                      
                                                             
              [0]() = 0                                      
                                                             
            [s](x1) = 1 + x1                                 
                                                             
     [plus](x1, x2) = 0                                      
                                                             
  [times^#](x1, x2) = 3 + 3*x1 + 3*x1^2                      
                                                             
            [c_1]() = 0                                      
                                                             
      [c_2](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2
                                                             
   [plus^#](x1, x2) = x2                                     
                                                             
            [c_3]() = 0                                      
                                                             
          [c_4](x1) = x1                                     
                                                             
            [c_5]() = 0                                      
                                                             
          [c_6](x1) = x1                                     
                                                             
  
  The following symbols are considered usable
  
    {times^#, plus^#}
  
  This order satisfies the following ordering constraints.
  
    [times^#(x, s(y))] =  3 + 3*x + 3*x^2         
                       >= 3 + 3*x + 3*x^2         
                       =  [times^#(x, y)]         
                                                  
    [times^#(x, s(y))] =  3 + 3*x + 3*x^2         
                       >  x                       
                       =  [plus^#(times(x, y), x)]
                                                  
     [plus^#(x, s(y))] =  1 + y                   
                       >  y                       
                       =  [c_4(plus^#(x, y))]     
                                                  
     [plus^#(s(x), y)] =  y                       
                       >= y                       
                       =  [c_6(plus^#(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(n^2)).

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

We use the processor 'polynomial interpretation' to orient
following rules strictly.

DPs:
  { 1: plus^#(s(x), y) -> c_6(plus^#(x, y))
  , 3: times^#(x, s(y)) -> plus^#(times(x, y), x) }

Sub-proof:
----------
  The following argument positions are considered usable:
  
    Uargs(c_4) = {1}, Uargs(c_6) = {1}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
    [times](x1, x2) = 2*x1*x2                                
                                                             
              [0]() = 0                                      
                                                             
            [s](x1) = 2 + x1                                 
                                                             
     [plus](x1, x2) = x1 + x2                                
                                                             
  [times^#](x1, x2) = 3 + 3*x1 + 2*x1*x2 + 3*x1^2            
                                                             
            [c_1]() = 0                                      
                                                             
      [c_2](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2
                                                             
   [plus^#](x1, x2) = x1                                     
                                                             
            [c_3]() = 0                                      
                                                             
          [c_4](x1) = x1                                     
                                                             
            [c_5]() = 0                                      
                                                             
          [c_6](x1) = x1                                     
                                                             
  
  The following symbols are considered usable
  
    {times, plus, times^#, plus^#}
  
  This order satisfies the following ordering constraints.
  
       [times(x, 0())] =                          
                       >=                         
                       =  [0()]                   
                                                  
      [times(x, s(y))] =  4*x + 2*x*y             
                       >= 2*x*y + x               
                       =  [plus(times(x, y), x)]  
                                                  
        [plus(x, 0())] =  x                       
                       >= x                       
                       =  [x]                     
                                                  
       [plus(x, s(y))] =  x + 2 + y               
                       >= 2 + x + y               
                       =  [s(plus(x, y))]         
                                                  
        [plus(0(), x)] =  x                       
                       >= x                       
                       =  [x]                     
                                                  
       [plus(s(x), y)] =  2 + x + y               
                       >= 2 + x + y               
                       =  [s(plus(x, y))]         
                                                  
    [times^#(x, s(y))] =  3 + 7*x + 2*x*y + 3*x^2 
                       >= 3 + 3*x + 2*x*y + 3*x^2 
                       =  [times^#(x, y)]         
                                                  
    [times^#(x, s(y))] =  3 + 7*x + 2*x*y + 3*x^2 
                       >  2*x*y                   
                       =  [plus^#(times(x, y), x)]
                                                  
     [plus^#(x, s(y))] =  x                       
                       >= x                       
                       =  [c_4(plus^#(x, y))]     
                                                  
     [plus^#(s(x), y)] =  2 + x                   
                       >  x                       
                       =  [c_6(plus^#(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:
  { times^#(x, s(y)) -> times^#(x, y)
  , times^#(x, s(y)) -> plus^#(times(x, y), x)
  , plus^#(x, s(y)) -> c_4(plus^#(x, y))
  , plus^#(s(x), y) -> c_6(plus^#(x, y)) }
Weak Trs:
  { times(x, 0()) -> 0()
  , times(x, s(y)) -> plus(times(x, y), x)
  , plus(x, 0()) -> x
  , plus(x, s(y)) -> s(plus(x, y))
  , plus(0(), x) -> x
  , plus(s(x), y) -> s(plus(x, 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.

{ times^#(x, s(y)) -> times^#(x, y)
, times^#(x, s(y)) -> plus^#(times(x, y), x)
, plus^#(x, s(y)) -> c_4(plus^#(x, y))
, plus^#(s(x), y) -> c_6(plus^#(x, y)) }

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

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