YES(?,O(n^2))

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

Strict Trs:
  { exp(x, 0()) -> s(0())
  , exp(x, s(y)) -> *(x, exp(x, y))
  , *(0(), y) -> 0()
  , *(s(x), y) -> +(y, *(x, y))
  , -(x, 0()) -> x
  , -(0(), y) -> 0()
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

We add following dependency tuples:

Strict DPs:
  { exp^#(x, 0()) -> c_1()
  , exp^#(x, s(y)) -> c_2(*^#(x, exp(x, y)), exp^#(x, y))
  , *^#(0(), y) -> c_3()
  , *^#(s(x), y) -> c_4(*^#(x, y))
  , -^#(x, 0()) -> c_5()
  , -^#(0(), y) -> c_6()
  , -^#(s(x), s(y)) -> c_7(-^#(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:
  { exp^#(x, 0()) -> c_1()
  , exp^#(x, s(y)) -> c_2(*^#(x, exp(x, y)), exp^#(x, y))
  , *^#(0(), y) -> c_3()
  , *^#(s(x), y) -> c_4(*^#(x, y))
  , -^#(x, 0()) -> c_5()
  , -^#(0(), y) -> c_6()
  , -^#(s(x), s(y)) -> c_7(-^#(x, y)) }
Weak Trs:
  { exp(x, 0()) -> s(0())
  , exp(x, s(y)) -> *(x, exp(x, y))
  , *(0(), y) -> 0()
  , *(s(x), y) -> +(y, *(x, y))
  , -(x, 0()) -> x
  , -(0(), y) -> 0()
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

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

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

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

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

{ exp^#(x, 0()) -> c_1()
, *^#(0(), y) -> c_3()
, -^#(x, 0()) -> c_5()
, -^#(0(), y) -> c_6() }

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

Strict DPs:
  { exp^#(x, s(y)) -> c_2(*^#(x, exp(x, y)), exp^#(x, y))
  , *^#(s(x), y) -> c_4(*^#(x, y))
  , -^#(s(x), s(y)) -> c_7(-^#(x, y)) }
Weak Trs:
  { exp(x, 0()) -> s(0())
  , exp(x, s(y)) -> *(x, exp(x, y))
  , *(0(), y) -> 0()
  , *(s(x), y) -> +(y, *(x, y))
  , -(x, 0()) -> x
  , -(0(), y) -> 0()
  , -(s(x), s(y)) -> -(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

We replace rewrite rules by usable rules:

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

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

Strict DPs:
  { exp^#(x, s(y)) -> c_2(*^#(x, exp(x, y)), exp^#(x, y))
  , *^#(s(x), y) -> c_4(*^#(x, y))
  , -^#(s(x), s(y)) -> c_7(-^#(x, y)) }
Weak Trs:
  { exp(x, 0()) -> s(0())
  , exp(x, s(y)) -> *(x, exp(x, y))
  , *(0(), y) -> 0()
  , *(s(x), y) -> +(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(exp) = {}, safe(0) = {}, safe(s) = {1}, safe(*) = {},
 safe(+) = {1, 2}, safe(exp^#) = {}, safe(c_2) = {},
 safe(*^#) = {2}, safe(c_4) = {}, safe(-^#) = {}, safe(c_7) = {}

and precedence

 exp > *, exp > *^#, exp^# > *, exp^# > *^#, -^# > *, -^# > *^#,
 exp ~ exp^#, exp ~ -^#, * ~ *^#, exp^# ~ -^# .

Following symbols are considered recursive:

 {exp, *, exp^#, *^#, -^#}

The recursion depth is 2.

Further, following argument filtering is employed:

 pi(exp) = [], pi(0) = [], pi(s) = [1], pi(*) = [2], pi(+) = [],
 pi(exp^#) = [1, 2], pi(c_2) = [1, 2], pi(*^#) = [1], pi(c_4) = [1],
 pi(-^#) = [1, 2], pi(c_7) = [1]

Usable defined function symbols are a subset of:

 {exp^#, *^#, -^#}

For your convenience, here are the satisfied ordering constraints:

   pi(exp^#(x, s(y))) = exp^#(x,  s(; y);)                     
                      > c_2(*^#(x;),  exp^#(x,  y;);)          
                      = pi(c_2(*^#(x, exp(x, y)), exp^#(x, y)))
                                                               
     pi(*^#(s(x), y)) = *^#(s(; x);)                           
                      > c_4(*^#(x;);)                          
                      = pi(c_4(*^#(x, y)))                     
                                                               
  pi(-^#(s(x), s(y))) = -^#(s(; x),  s(; y);)                  
                      > c_7(-^#(x,  y;);)                      
                      = pi(c_7(-^#(x, y)))                     
                                                               

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