YES(?,O(n^3))

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

Strict Trs:
  { fac(s(x)) -> *(fac(p(s(x))), s(x))
  , p(s(s(x))) -> s(p(s(x)))
  , p(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

We add following dependency tuples:

Strict DPs:
  { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x)))
  , p^#(s(s(x))) -> c_2(p^#(s(x)))
  , p^#(s(0())) -> c_3() }

and mark the set of starting terms.

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

Strict DPs:
  { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x)))
  , p^#(s(s(x))) -> c_2(p^#(s(x)))
  , p^#(s(0())) -> c_3() }
Weak Trs:
  { fac(s(x)) -> *(fac(p(s(x))), s(x))
  , p(s(s(x))) -> s(p(s(x)))
  , p(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

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

  DPs:
    { 1: fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x)))
    , 2: p^#(s(s(x))) -> c_2(p^#(s(x)))
    , 3: p^#(s(0())) -> c_3() }

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

Strict DPs:
  { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x)))
  , p^#(s(s(x))) -> c_2(p^#(s(x))) }
Weak DPs: { p^#(s(0())) -> c_3() }
Weak Trs:
  { fac(s(x)) -> *(fac(p(s(x))), s(x))
  , p(s(s(x))) -> s(p(s(x)))
  , p(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ p^#(s(0())) -> c_3() }

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

Strict DPs:
  { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x)))
  , p^#(s(s(x))) -> c_2(p^#(s(x))) }
Weak Trs:
  { fac(s(x)) -> *(fac(p(s(x))), s(x))
  , p(s(s(x))) -> s(p(s(x)))
  , p(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

We replace rewrite rules by usable rules:

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

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

Strict DPs:
  { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x)))
  , p^#(s(s(x))) -> c_2(p^#(s(x))) }
Weak Trs:
  { p(s(s(x))) -> s(p(s(x)))
  , p(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

The following argument positions are usable:
  Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}

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

                  [0 0 1 0]      [0]               
        [s](x1) = [0 1 1 0] x1 + [0]               
                  [0 0 1 0]      [1]               
                  [0 1 0 0]      [0]               
                                                   
                  [0 1 0 0]      [0]               
        [p](x1) = [0 0 0 1] x1 + [0]               
                  [1 0 0 0]      [0]               
                  [0 1 0 0]      [0]               
                                                   
                  [0]                              
            [0] = [0]                              
                  [0]                              
                  [0]                              
                                                   
                  [0 1 1 0]      [0]               
    [fac^#](x1) = [0 0 0 0] x1 + [0]               
                  [0 0 0 0]      [0]               
                  [0 0 0 0]      [0]               
                                                   
                  [1 0 0 0]      [1 0 0 0]      [0]
  [c_1](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
                  [0 0 0 0]      [0 0 0 0]      [0]
                  [0 0 0 0]      [0 0 0 0]      [0]
                                                   
                  [1 0 0 0]      [0]               
      [p^#](x1) = [0 0 0 0] x1 + [0]               
                  [0 0 0 0]      [0]               
                  [0 0 0 0]      [0]               
                                                   
                  [1 0 0 0]      [0]               
      [c_2](x1) = [0 0 0 0] x1 + [0]               
                  [0 0 0 0]      [0]               
                  [0 0 0 0]      [0]               

This order satisfies following ordering constraints:

    [p(s(s(x)))] =  [0 1 2 0]     [1]               
                    [0 1 1 0] x + [0]               
                    [0 0 1 0]     [1]               
                    [0 1 2 0]     [1]               
                 >  [0 0 1 0]     [0]               
                    [0 1 1 0] x + [0]               
                    [0 0 1 0]     [1]               
                    [0 1 0 0]     [0]               
                 =  [s(p(s(x)))]                    
                                                    
     [p(s(0()))] =  [0]                             
                    [0]                             
                    [0]                             
                    [0]                             
                 >= [0]                             
                    [0]                             
                    [0]                             
                    [0]                             
                 =  [0()]                           
                                                    
   [fac^#(s(x))] =  [0 1 2 0]     [1]               
                    [0 0 0 0] x + [0]               
                    [0 0 0 0]     [0]               
                    [0 0 0 0]     [0]               
                 >  [0 1 2 0]     [0]               
                    [0 0 0 0] x + [0]               
                    [0 0 0 0]     [0]               
                    [0 0 0 0]     [0]               
                 =  [c_1(fac^#(p(s(x))), p^#(s(x)))]
                                                    
  [p^#(s(s(x)))] =  [0 0 1 0]     [1]               
                    [0 0 0 0] x + [0]               
                    [0 0 0 0]     [0]               
                    [0 0 0 0]     [0]               
                 >  [0 0 1 0]     [0]               
                    [0 0 0 0] x + [0]               
                    [0 0 0 0]     [0]               
                    [0 0 0 0]     [0]               
                 =  [c_2(p^#(s(x)))]                
                                                    

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