YES(?,O(n^2))

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

Strict Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , gcd(0(), y) -> y
  , gcd(s(x), 0()) -> s(x)
  , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
  , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
  , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

We add following dependency tuples:

Strict DPs:
  { le^#(0(), y) -> c_1()
  , le^#(s(x), 0()) -> c_2()
  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , minus^#(x, 0()) -> c_4()
  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
  , gcd^#(0(), y) -> c_6()
  , gcd^#(s(x), 0()) -> c_7()
  , gcd^#(s(x), s(y)) ->
    c_8(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x))
  , if_gcd^#(true(), s(x), s(y)) ->
    c_9(gcd^#(minus(x, y), s(y)), minus^#(x, y))
  , if_gcd^#(false(), s(x), s(y)) ->
    c_10(gcd^#(minus(y, x), s(x)), minus^#(y, x)) }

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:
  { le^#(0(), y) -> c_1()
  , le^#(s(x), 0()) -> c_2()
  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , minus^#(x, 0()) -> c_4()
  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
  , gcd^#(0(), y) -> c_6()
  , gcd^#(s(x), 0()) -> c_7()
  , gcd^#(s(x), s(y)) ->
    c_8(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x))
  , if_gcd^#(true(), s(x), s(y)) ->
    c_9(gcd^#(minus(x, y), s(y)), minus^#(x, y))
  , if_gcd^#(false(), s(x), s(y)) ->
    c_10(gcd^#(minus(y, x), s(x)), minus^#(y, x)) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , gcd(0(), y) -> y
  , gcd(s(x), 0()) -> s(x)
  , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
  , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
  , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

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

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

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

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

{ le^#(0(), y) -> c_1()
, le^#(s(x), 0()) -> c_2()
, minus^#(x, 0()) -> c_4()
, gcd^#(0(), y) -> c_6()
, gcd^#(s(x), 0()) -> c_7() }

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

Strict DPs:
  { le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
  , gcd^#(s(x), s(y)) ->
    c_8(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x))
  , if_gcd^#(true(), s(x), s(y)) ->
    c_9(gcd^#(minus(x, y), s(y)), minus^#(x, y))
  , if_gcd^#(false(), s(x), s(y)) ->
    c_10(gcd^#(minus(y, x), s(x)), minus^#(y, x)) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , gcd(0(), y) -> y
  , gcd(s(x), 0()) -> s(x)
  , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
  , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
  , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { le(0(), y) -> true()
    , le(s(x), 0()) -> false()
    , le(s(x), s(y)) -> le(x, y)
    , minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y) }

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

Strict DPs:
  { le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
  , gcd^#(s(x), s(y)) ->
    c_8(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x))
  , if_gcd^#(true(), s(x), s(y)) ->
    c_9(gcd^#(minus(x, y), s(y)), minus^#(x, y))
  , if_gcd^#(false(), s(x), s(y)) ->
    c_10(gcd^#(minus(y, x), s(x)), minus^#(y, x)) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

The following argument positions are usable:
  Uargs(c_3) = {1}, Uargs(c_5) = {1}, Uargs(c_8) = {1, 2},
  Uargs(c_9) = {1, 2}, Uargs(c_10) = {1, 2}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

            [le](x1, x2) = [0]                      
                           [0]                      
                                                    
                     [0] = [0]                      
                           [0]                      
                                                    
                  [true] = [0]                      
                           [0]                      
                                                    
                 [s](x1) = [1 3] x1 + [0]           
                           [0 1]      [2]           
                                                    
                 [false] = [0]                      
                           [0]                      
                                                    
         [minus](x1, x2) = [1 0] x1 + [0]           
                           [0 1]      [0]           
                                                    
          [le^#](x1, x2) = [0 1] x2 + [0]           
                           [0 0]      [0]           
                                                    
               [c_3](x1) = [1 0] x1 + [1]           
                           [0 0]      [0]           
                                                    
       [minus^#](x1, x2) = [0 1] x1 + [0]           
                           [0 0]      [1]           
                                                    
               [c_5](x1) = [1 1] x1 + [0]           
                           [0 0]      [1]           
                                                    
         [gcd^#](x1, x2) = [1 1] x1 + [1 0] x2 + [1]
                           [2 0]      [0 0]      [0]
                                                    
           [c_8](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                           [0 0]      [0 0]      [0]
                                                    
  [if_gcd^#](x1, x2, x3) = [1 0] x2 + [1 0] x3 + [2]
                           [0 0]      [0 0]      [0]
                                                    
           [c_9](x1, x2) = [1 0] x1 + [2 0] x2 + [0]
                           [0 0]      [0 0]      [0]
                                                    
          [c_10](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                           [0 0]      [0 0]      [0]

This order satisfies following ordering constraints:

                  [minus(x, 0())] =  [1 0] x + [0]                                    
                                     [0 1]     [0]                                    
                                  >= [1 0] x + [0]                                    
                                     [0 1]     [0]                                    
                                  =  [x]                                              
                                                                                      
              [minus(s(x), s(y))] =  [1 3] x + [0]                                    
                                     [0 1]     [2]                                    
                                  >= [1 0] x + [0]                                    
                                     [0 1]     [0]                                    
                                  =  [minus(x, y)]                                    
                                                                                      
               [le^#(s(x), s(y))] =  [0 1] y + [2]                                    
                                     [0 0]     [0]                                    
                                  >  [0 1] y + [1]                                    
                                     [0 0]     [0]                                    
                                  =  [c_3(le^#(x, y))]                                
                                                                                      
            [minus^#(s(x), s(y))] =  [0 1] x + [2]                                    
                                     [0 0]     [1]                                    
                                  >  [0 1] x + [1]                                    
                                     [0 0]     [1]                                    
                                  =  [c_5(minus^#(x, y))]                             
                                                                                      
              [gcd^#(s(x), s(y))] =  [1 3] y + [1 4] x + [3]                          
                                     [0 0]     [2 6]     [0]                          
                                  >  [1 3] y + [1 4] x + [2]                          
                                     [0 0]     [0 0]     [0]                          
                                  =  [c_8(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x))]
                                                                                      
   [if_gcd^#(true(), s(x), s(y))] =  [1 3] y + [1 3] x + [2]                          
                                     [0 0]     [0 0]     [0]                          
                                  >  [1 3] y + [1 3] x + [1]                          
                                     [0 0]     [0 0]     [0]                          
                                  =  [c_9(gcd^#(minus(x, y), s(y)), minus^#(x, y))]   
                                                                                      
  [if_gcd^#(false(), s(x), s(y))] =  [1 3] y + [1 3] x + [2]                          
                                     [0 0]     [0 0]     [0]                          
                                  >  [1 2] y + [1 3] x + [1]                          
                                     [0 0]     [0 0]     [0]                          
                                  =  [c_10(gcd^#(minus(y, x), s(x)), minus^#(y, x))]  
                                                                                      

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