YES(?,O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(?,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(n^2))

We add 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(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(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(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(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(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(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(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(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(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(n^2))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS)' as induced by the safe mapping

 safe(-) = {}, safe(0) = {}, safe(s) = {1}, safe(-^#) = {2},
 safe(lt^#) = {2}, safe(div^#) = {2}, 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(-^#) = [1], pi(lt^#) = [1],
 pi(div^#) = [1], pi(c_1) = [1], pi(c_2) = [1], pi(c_3) = [1, 2, 3]

Usable defined function symbols are a subset of:

 {-, -^#, lt^#, 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))                                         
                                                                               

Hurray, we answered YES(?,O(n^2))