YES(?,O(n^2))

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

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

We add following dependency tuples:

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

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

  DPs:
    { 1: add^#(0(), x) -> c_1()
    , 2: add^#(s(x), y) -> c_2(add^#(x, y))
    , 3: mult^#(0(), x) -> c_3()
    , 4: mult^#(s(x), y) -> c_4(add^#(y, mult(x, y)), mult^#(x, y)) }

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

Strict DPs:
  { add^#(s(x), y) -> c_2(add^#(x, y))
  , mult^#(s(x), y) -> c_4(add^#(y, mult(x, y)), mult^#(x, y)) }
Weak DPs:
  { add^#(0(), x) -> c_1()
  , mult^#(0(), x) -> c_3() }
Weak Trs:
  { add(0(), x) -> x
  , add(s(x), y) -> s(add(x, y))
  , mult(0(), x) -> 0()
  , mult(s(x), y) -> add(y, mult(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.

{ add^#(0(), x) -> c_1()
, mult^#(0(), x) -> c_3() }

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

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

and precedence

 add > add^#, mult > add^#, mult^# > add^#, add ~ mult,
 add ~ mult^#, mult ~ mult^# .

Following symbols are considered recursive:

 {add, mult, add^#, mult^#}

The recursion depth is 2.

Further, following argument filtering is employed:

 pi(add) = 1, pi(0) = [], pi(s) = [1], pi(mult) = [],
 pi(add^#) = [1], pi(c_2) = [1], pi(mult^#) = [1, 2],
 pi(c_4) = [1, 2]

Usable defined function symbols are a subset of:

 {add^#, mult^#}

For your convenience, here are the satisfied ordering constraints:

   pi(add^#(s(x), y)) = add^#(s(; x);)                             
                      > c_2(add^#(x;);)                            
                      = pi(c_2(add^#(x, y)))                       
                                                                   
  pi(mult^#(s(x), y)) = mult^#(s(; x),  y;)                        
                      > c_4(add^#(y;),  mult^#(x,  y;);)           
                      = pi(c_4(add^#(y, mult(x, y)), mult^#(x, y)))
                                                                   

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