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

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

We add the following dependency tuples:

Strict DPs:
  { pred^#(s(x)) -> c_1()
  , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , minus^#(x, 0()) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , quot^#(0(), s(y)) -> c_5()
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))
  , log^#(s(0())) -> c_7() }

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:
  { pred^#(s(x)) -> c_1()
  , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , minus^#(x, 0()) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , quot^#(0(), s(y)) -> c_5()
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))
  , log^#(s(0())) -> c_7() }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

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

  DPs:
    { 1: pred^#(s(x)) -> c_1()
    , 2: minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
    , 3: minus^#(x, 0()) -> c_3()
    , 4: quot^#(s(x), s(y)) ->
         c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , 5: quot^#(0(), s(y)) -> c_5()
    , 6: log^#(s(s(x))) ->
         c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))
    , 7: log^#(s(0())) -> c_7() }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak DPs:
  { pred^#(s(x)) -> c_1()
  , minus^#(x, 0()) -> c_3()
  , quot^#(0(), s(y)) -> c_5()
  , log^#(s(0())) -> c_7() }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(0())) -> 0() }
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.

{ pred^#(s(x)) -> c_1()
, minus^#(x, 0()) -> c_3()
, quot^#(0(), s(y)) -> c_5()
, log^#(s(0())) -> c_7() }

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

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

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

  { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0() }
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

  { log^#(s(s(x))) ->
    c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }

and lower component

  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) }

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

{ log^#(s(s(x))) -> quot^#(x, s(s(0())))
, log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }

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:
    { log^#(s(s(x))) ->
      c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
  Weak Trs:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }
  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: log^#(s(s(x))) ->
         c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
  Trs: { pred(s(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(pred) = {}, safe(s) = {1}, safe(minus) = {2}, safe(0) = {},
     safe(quot) = {}, safe(quot^#) = {}, safe(log^#) = {},
     safe(c_3) = {}
    
    and precedence
    
     minus > pred .
    
    Following symbols are considered recursive:
    
     {log^#}
    
    The recursion depth is 1.
    
    Further, following argument filtering is employed:
    
     pi(pred) = 1, pi(s) = [1], pi(minus) = 1, pi(0) = [], pi(quot) = 1,
     pi(quot^#) = [], pi(log^#) = [1], pi(c_3) = [1, 2]
    
    Usable defined function symbols are a subset of:
    
     {pred, minus, quot, quot^#, log^#}
    
    For your convenience, here are the satisfied ordering constraints:
    
        pi(log^#(s(s(x)))) =  log^#(s(; s(; x));)                                        
                           >  c_3(log^#(s(; x);),  quot^#();)                            
                           =  pi(c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))))
                                                                                         
            pi(pred(s(x))) =  s(; x)                                                     
                           >  x                                                          
                           =  pi(x)                                                      
                                                                                         
        pi(minus(x, s(y))) =  x                                                          
                           >= x                                                          
                           =  pi(pred(minus(x, y)))                                      
                                                                                         
         pi(minus(x, 0())) =  x                                                          
                           >= x                                                          
                           =  pi(x)                                                      
                                                                                         
      pi(quot(s(x), s(y))) =  s(; x)                                                     
                           >= s(; x)                                                     
                           =  pi(s(quot(minus(x, y), s(y))))                             
                                                                                         
       pi(quot(0(), s(y))) =  0()                                                        
                           >= 0()                                                        
                           =  pi(0())                                                    
                                                                                         
  
  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:
    { log^#(s(s(x))) ->
      c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
  Weak Trs:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }
  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.
  
  { log^#(s(s(x))) ->
    c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }
  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:
  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) }
Weak DPs:
  { log^#(s(s(x))) -> quot^#(x, s(s(0())))
  , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

  { quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) -> quot^#(x, s(s(0())))
  , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }

and lower component

  { minus^#(x, s(y)) -> c_1(minus^#(x, y)) }

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

{ quot^#(s(x), s(y)) -> minus^#(x, y)
, quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
, log^#(s(s(x))) -> quot^#(x, s(s(0())))
, log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }

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:
    { quot^#(s(x), s(y)) ->
      c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) }
  Weak DPs:
    { log^#(s(s(x))) -> quot^#(x, s(s(0())))
    , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
  Weak Trs:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }
  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: quot^#(s(x), s(y)) ->
         c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , 2: log^#(s(s(x))) -> quot^#(x, s(s(0())))
    , 3: log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
  Trs: { pred(s(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(pred) = {}, safe(s) = {1}, safe(minus) = {1, 2}, safe(0) = {},
     safe(quot) = {}, safe(minus^#) = {}, safe(quot^#) = {2},
     safe(log^#) = {}, safe(c_2) = {}
    
    and precedence
    
     quot^# ~ log^# .
    
    Following symbols are considered recursive:
    
     {quot^#, log^#}
    
    The recursion depth is 1.
    
    Further, following argument filtering is employed:
    
     pi(pred) = 1, pi(s) = [1], pi(minus) = 1, pi(0) = [], pi(quot) = 1,
     pi(minus^#) = [], pi(quot^#) = [1, 2], pi(log^#) = [1],
     pi(c_2) = [1, 2]
    
    Usable defined function symbols are a subset of:
    
     {pred, minus, quot, minus^#, quot^#, log^#}
    
    For your convenience, here are the satisfied ordering constraints:
    
      pi(quot^#(s(x), s(y))) =  quot^#(s(; x); s(; y))                           
                             >  c_2(quot^#(x; s(; y)),  minus^#();)              
                             =  pi(c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)))
                                                                                 
          pi(log^#(s(s(x)))) =  log^#(s(; s(; x));)                              
                             >  quot^#(x; s(; s(; 0())))                         
                             =  pi(quot^#(x, s(s(0()))))                         
                                                                                 
          pi(log^#(s(s(x)))) =  log^#(s(; s(; x));)                              
                             >  log^#(s(; x);)                                   
                             =  pi(log^#(s(quot(x, s(s(0()))))))                 
                                                                                 
              pi(pred(s(x))) =  s(; x)                                           
                             >  x                                                
                             =  pi(x)                                            
                                                                                 
          pi(minus(x, s(y))) =  x                                                
                             >= x                                                
                             =  pi(pred(minus(x, y)))                            
                                                                                 
           pi(minus(x, 0())) =  x                                                
                             >= x                                                
                             =  pi(x)                                            
                                                                                 
        pi(quot(s(x), s(y))) =  s(; x)                                           
                             >= s(; x)                                           
                             =  pi(s(quot(minus(x, y), s(y))))                   
                                                                                 
         pi(quot(0(), s(y))) =  0()                                              
                             >= 0()                                              
                             =  pi(0())                                          
                                                                                 
  
  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:
    { quot^#(s(x), s(y)) ->
      c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , log^#(s(s(x))) -> quot^#(x, s(s(0())))
    , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
  Weak Trs:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }
  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.
  
  { quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) -> quot^#(x, s(s(0())))
  , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }
  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^1)).

Strict DPs: { minus^#(x, s(y)) -> c_1(minus^#(x, y)) }
Weak DPs:
  { quot^#(s(x), s(y)) -> minus^#(x, y)
  , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
  , log^#(s(s(x))) -> quot^#(x, s(s(0())))
  , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

DPs:
  { 1: minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , 2: quot^#(s(x), s(y)) -> minus^#(x, y) }
Trs:
  { minus(x, s(y)) -> pred(minus(x, y))
  , quot(0(), s(y)) -> 0() }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [pred](x1) = [0]         
                                    
              [s](x1) = [1] x1 + [1]
                                    
      [minus](x1, x2) = [4]         
                                    
                  [0] = [1]         
                                    
       [quot](x1, x2) = [1] x1 + [7]
                                    
    [minus^#](x1, x2) = [1] x2 + [0]
                                    
     [quot^#](x1, x2) = [2] x2 + [0]
                                    
          [log^#](x1) = [6]         
                                    
            [c_1](x1) = [1] x1 + [0]
  
  The order satisfies the following ordering constraints:
  
            [pred(s(x))] =  [0]                           
                         ?  [1] x + [0]                   
                         =  [x]                           
                                                          
        [minus(x, s(y))] =  [4]                           
                         >  [0]                           
                         =  [pred(minus(x, y))]           
                                                          
         [minus(x, 0())] =  [4]                           
                         ?  [1] x + [0]                   
                         =  [x]                           
                                                          
      [quot(s(x), s(y))] =  [1] x + [8]                   
                         ?  [12]                          
                         =  [s(quot(minus(x, y), s(y)))]  
                                                          
       [quot(0(), s(y))] =  [8]                           
                         >  [1]                           
                         =  [0()]                         
                                                          
      [minus^#(x, s(y))] =  [1] y + [1]                   
                         >  [1] y + [0]                   
                         =  [c_1(minus^#(x, y))]          
                                                          
    [quot^#(s(x), s(y))] =  [2] y + [2]                   
                         >  [1] y + [0]                   
                         =  [minus^#(x, y)]               
                                                          
    [quot^#(s(x), s(y))] =  [2] y + [2]                   
                         >= [2] y + [2]                   
                         =  [quot^#(minus(x, y), s(y))]   
                                                          
        [log^#(s(s(x)))] =  [6]                           
                         >= [6]                           
                         =  [quot^#(x, s(s(0())))]        
                                                          
        [log^#(s(s(x)))] =  [6]                           
                         >= [6]                           
                         =  [log^#(s(quot(x, s(s(0())))))]
                                                          

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:
  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) -> minus^#(x, y)
  , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
  , log^#(s(s(x))) -> quot^#(x, s(s(0())))
  , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0() }
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.

{ minus^#(x, s(y)) -> c_1(minus^#(x, y))
, quot^#(s(x), s(y)) -> minus^#(x, y)
, quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
, log^#(s(s(x))) -> quot^#(x, s(s(0())))
, log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) }

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

Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0() }
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))