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

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

Strict Trs:
  { -(x, 0()) -> x
  , -(0(), s(y)) -> 0()
  , -(s(x), s(y)) -> -(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , lt(s(x), s(y)) -> lt(x, y)
  , if(false(), x, y) -> y
  , if(true(), x, y) -> x
  , div(x, 0()) -> 0()
  , div(0(), y) -> 0()
  , div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add the following dependency tuples:

Strict DPs:
  { -^#(x, 0()) -> c_1()
  , -^#(0(), s(y)) -> c_2()
  , -^#(s(x), s(y)) -> c_3(-^#(x, y))
  , lt^#(x, 0()) -> c_4()
  , lt^#(0(), s(y)) -> c_5()
  , lt^#(s(x), s(y)) -> c_6(lt^#(x, y))
  , if^#(false(), x, y) -> c_7()
  , if^#(true(), x, y) -> c_8()
  , div^#(x, 0()) -> c_9()
  , div^#(0(), y) -> c_10()
  , div^#(s(x), s(y)) ->
    c_11(if^#(lt(x, y), 0(), s(div(-(x, y), s(y)))),
         lt^#(x, y),
         div^#(-(x, y), s(y)),
         -^#(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^2)).

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

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

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

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

Strict DPs:
  { -^#(s(x), s(y)) -> c_3(-^#(x, y))
  , lt^#(s(x), s(y)) -> c_6(lt^#(x, y))
  , div^#(s(x), s(y)) ->
    c_11(if^#(lt(x, y), 0(), s(div(-(x, y), s(y)))),
         lt^#(x, y),
         div^#(-(x, y), s(y)),
         -^#(x, y)) }
Weak DPs:
  { -^#(x, 0()) -> c_1()
  , -^#(0(), s(y)) -> c_2()
  , lt^#(x, 0()) -> c_4()
  , lt^#(0(), s(y)) -> c_5()
  , if^#(false(), x, y) -> c_7()
  , if^#(true(), x, y) -> c_8()
  , div^#(x, 0()) -> c_9()
  , div^#(0(), y) -> c_10() }
Weak Trs:
  { -(x, 0()) -> x
  , -(0(), s(y)) -> 0()
  , -(s(x), s(y)) -> -(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , lt(s(x), s(y)) -> lt(x, y)
  , if(false(), x, y) -> y
  , if(true(), x, y) -> x
  , div(x, 0()) -> 0()
  , div(0(), y) -> 0()
  , div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(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.

{ -^#(x, 0()) -> c_1()
, -^#(0(), s(y)) -> c_2()
, lt^#(x, 0()) -> c_4()
, lt^#(0(), s(y)) -> c_5()
, if^#(false(), x, y) -> c_7()
, if^#(true(), x, y) -> c_8()
, div^#(x, 0()) -> c_9()
, div^#(0(), y) -> c_10() }

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

Strict DPs:
  { -^#(s(x), s(y)) -> c_3(-^#(x, y))
  , lt^#(s(x), s(y)) -> c_6(lt^#(x, y))
  , div^#(s(x), s(y)) ->
    c_11(if^#(lt(x, y), 0(), s(div(-(x, y), s(y)))),
         lt^#(x, y),
         div^#(-(x, y), s(y)),
         -^#(x, y)) }
Weak Trs:
  { -(x, 0()) -> x
  , -(0(), s(y)) -> 0()
  , -(s(x), s(y)) -> -(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , lt(s(x), s(y)) -> lt(x, y)
  , if(false(), x, y) -> y
  , if(true(), x, y) -> x
  , div(x, 0()) -> 0()
  , div(0(), y) -> 0()
  , div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

  { div^#(s(x), s(y)) ->
    c_11(if^#(lt(x, y), 0(), s(div(-(x, y), s(y)))),
         lt^#(x, y),
         div^#(-(x, y), s(y)),
         -^#(x, y)) }

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

Strict DPs:
  { -^#(s(x), s(y)) -> c_1(-^#(x, y))
  , lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , div^#(s(x), s(y)) ->
    c_3(lt^#(x, y), div^#(-(x, y), s(y)), -^#(x, y)) }
Weak Trs:
  { -(x, 0()) -> x
  , -(0(), s(y)) -> 0()
  , -(s(x), s(y)) -> -(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , lt(s(x), s(y)) -> lt(x, y)
  , if(false(), x, y) -> y
  , if(true(), x, y) -> x
  , div(x, 0()) -> 0()
  , div(0(), y) -> 0()
  , div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

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

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

Strict DPs:
  { -^#(s(x), s(y)) -> c_1(-^#(x, y))
  , lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , div^#(s(x), s(y)) ->
    c_3(lt^#(x, y), div^#(-(x, y), s(y)), -^#(x, y)) }
Weak Trs:
  { -(x, 0()) -> x
  , -(0(), s(y)) -> 0()
  , -(s(x), s(y)) -> -(x, 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: -^#(s(x), s(y)) -> c_1(-^#(x, y))
  , 2: lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , 3: div^#(s(x), s(y)) ->
       c_3(lt^#(x, y), div^#(-(x, y), s(y)), -^#(x, y)) }
Trs: { -(s(x), s(y)) -> -(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(-) = {}, safe(0) = {}, safe(s) = {1}, safe(lt) = {},
   safe(false) = {}, safe(true) = {}, safe(if) = {}, safe(div) = {},
   safe(-^#) = {2}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {},
   safe(lt^#) = {2}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {},
   safe(if^#) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(div^#) = {2},
   safe(c_9) = {}, safe(c_10) = {}, safe(c_11) = {}, safe(c) = {},
   safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}
  
  and precedence
  
   - > -^#, - > lt^#, div^# > -^#, div^# > lt^#, - ~ div^#,
   -^# ~ lt^# .
  
  Following symbols are considered recursive:
  
   {-^#, lt^#, div^#}
  
  The recursion depth is 2.
  
  Further, following argument filtering is employed:
  
   pi(-) = 1, pi(0) = [], pi(s) = [1], pi(lt) = [], pi(false) = [],
   pi(true) = [], pi(if) = [], pi(div) = [], pi(-^#) = [1],
   pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(lt^#) = [1],
   pi(c_4) = [], pi(c_5) = [], pi(c_6) = [], pi(if^#) = [],
   pi(c_7) = [], pi(c_8) = [], pi(div^#) = [1], pi(c_9) = [],
   pi(c_10) = [], pi(c_11) = [], pi(c) = [], pi(c_1) = [1],
   pi(c_2) = [1], pi(c_3) = [1, 2, 3]
  
  Usable defined function symbols are a subset of:
  
   {-, -^#, lt^#, if^#, div^#}
  
  For your convenience, here are the satisfied ordering constraints:
  
      pi(-^#(s(x), s(y))) =  -^#(s(; x);)                                        
                          >  c_1(-^#(x;);)                                       
                          =  pi(c_1(-^#(x, y)))                                  
                                                                                 
     pi(lt^#(s(x), s(y))) =  lt^#(s(; x);)                                       
                          >  c_2(lt^#(x;);)                                      
                          =  pi(c_2(lt^#(x, y)))                                 
                                                                                 
    pi(div^#(s(x), s(y))) =  div^#(s(; x);)                                      
                          >  c_3(lt^#(x;),  div^#(x;),  -^#(x;);)                
                          =  pi(c_3(lt^#(x, y), div^#(-(x, y), s(y)), -^#(x, y)))
                                                                                 
            pi(-(x, 0())) =  x                                                   
                          >= x                                                   
                          =  pi(x)                                               
                                                                                 
         pi(-(0(), s(y))) =  0()                                                 
                          >= 0()                                                 
                          =  pi(0())                                             
                                                                                 
        pi(-(s(x), s(y))) =  s(; x)                                              
                          >  x                                                   
                          =  pi(-(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:
  { -^#(s(x), s(y)) -> c_1(-^#(x, y))
  , lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , div^#(s(x), s(y)) ->
    c_3(lt^#(x, y), div^#(-(x, y), s(y)), -^#(x, y)) }
Weak Trs:
  { -(x, 0()) -> x
  , -(0(), s(y)) -> 0()
  , -(s(x), s(y)) -> -(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.

{ -^#(s(x), s(y)) -> c_1(-^#(x, y))
, lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
, div^#(s(x), s(y)) ->
  c_3(lt^#(x, y), div^#(-(x, y), s(y)), -^#(x, y)) }

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

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